Theorem cvcon3t 5716

Description: Contraposition law for the covers relation.

Assertion

Ref	Expression
cvcon3t	|- ((A e. CH /\ B e. CH) -> (A <o B <-> (_|_` B) <o (_|_` A)))

Proof of Theorem cvcon3t

Step	Hyp	Ref	Expression
1		chpsscon3t 5420	. . 3 |- ((A e. CH /\ B e. CH) -> (A (. B <-> (_|_` B) (. (_|_` A)))
2		chpsscon3t 5420	. . . . . . . . . 10 |- ((A e. CH /\ x e. CH) -> (A (. x <-> (_|_` x) (. (_|_` A)))
3	2	adantlr 310	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (A (. x <-> (_|_` x) (. (_|_` A)))
4		chpsscon3t 5420	. . . . . . . . . . 11 |- ((x e. CH /\ B e. CH) -> (x (. B <-> (_|_` B) (. (_|_` x)))
5	4	ancoms 334	. . . . . . . . . 10 |- ((B e. CH /\ x e. CH) -> (x (. B <-> (_|_` B) (. (_|_` x)))
6	5	adantll 309	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (x (. B <-> (_|_` B) (. (_|_` x)))
7	3, 6	anbi12d 476	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> ((A (. x /\ x (. B) <-> ((_|_` x) (. (_|_` A) /\ (_|_` B) (. (_|_` x))))
8		psseq2 1560	. . . . . . . . . . . . . 14 |- (y = (_|_` x) -> ((_|_` B) (. y <-> (_|_` B) (. (_|_` x)))
9		psseq1 1559	. . . . . . . . . . . . . 14 |- (y = (_|_` x) -> (y (. (_|_` A) <-> (_|_` x) (. (_|_` A)))
10	8, 9	anbi12d 476	. . . . . . . . . . . . 13 |- (y = (_|_` x) -> (((_|_` B) (. y /\ y (. (_|_` A)) <-> ((_|_` B) (. (_|_` x) /\ (_|_` x) (. (_|_` A))))
11	10	rcla4ev 1403	. . . . . . . . . . . 12 |- (((_|_` x) e. CH /\ ((_|_` B) (. (_|_` x) /\ (_|_` x) (. (_|_` A))) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))
12		choclt 5191	. . . . . . . . . . . 12 |- (x e. CH -> (_|_` x) e. CH)
13	11, 12	sylan 343	. . . . . . . . . . 11 |- ((x e. CH /\ ((_|_` B) (. (_|_` x) /\ (_|_` x) (. (_|_` A))) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))
14	13	exp 291	. . . . . . . . . 10 |- (x e. CH -> (((_|_` B) (. (_|_` x) /\ (_|_` x) (. (_|_` A)) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
15	14	ancomsd 335	. . . . . . . . 9 |- (x e. CH -> (((_|_` x) (. (_|_` A) /\ (_|_` B) (. (_|_` x)) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
16	15	adantl 305	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (((_|_` x) (. (_|_` A) /\ (_|_` B) (. (_|_` x)) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
17	7, 16	sylbid 178	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> ((A (. x /\ x (. B) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
18	17	exp 291	. . . . . 6 |- ((A e. CH /\ B e. CH) -> (x e. CH -> ((A (. x /\ x (. B) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))))
19	18	r19.23adv 1286	. . . . 5 |- ((A e. CH /\ B e. CH) -> (E.x e. CH (A (. x /\ x (. B) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
20		chpsscon1t 5421	. . . . . . . . . 10 |- ((B e. CH /\ y e. CH) -> ((_|_` B) (. y <-> (_|_` y) (. B))
21	20	adantll 309	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((_|_` B) (. y <-> (_|_` y) (. B))
22		chpsscon2t 5422	. . . . . . . . . . 11 |- ((y e. CH /\ A e. CH) -> (y (. (_|_` A) <-> A (. (_|_` y)))
23	22	ancoms 334	. . . . . . . . . 10 |- ((A e. CH /\ y e. CH) -> (y (. (_|_` A) <-> A (. (_|_` y)))
24	23	adantlr 310	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (y (. (_|_` A) <-> A (. (_|_` y)))
25	21, 24	anbi12d 476	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (((_|_` B) (. y /\ y (. (_|_` A)) <-> ((_|_` y) (. B /\ A (. (_|_` y))))
26		psseq2 1560	. . . . . . . . . . . . . 14 |- (x = (_|_` y) -> (A (. x <-> A (. (_|_` y)))
27		psseq1 1559	. . . . . . . . . . . . . 14 |- (x = (_|_` y) -> (x (. B <-> (_|_` y) (. B))
28	26, 27	anbi12d 476	. . . . . . . . . . . . 13 |- (x = (_|_` y) -> ((A (. x /\ x (. B) <-> (A (. (_|_` y) /\ (_|_` y) (. B)))
29	28	rcla4ev 1403	. . . . . . . . . . . 12 |- (((_|_` y) e. CH /\ (A (. (_|_` y) /\ (_|_` y) (. B)) -> E.x e. CH (A (. x /\ x (. B))
30		choclt 5191	. . . . . . . . . . . 12 |- (y e. CH -> (_|_` y) e. CH)
31	29, 30	sylan 343	. . . . . . . . . . 11 |- ((y e. CH /\ (A (. (_|_` y) /\ (_|_` y) (. B)) -> E.x e. CH (A (. x /\ x (. B))
32	31	exp 291	. . . . . . . . . 10 |- (y e. CH -> ((A (. (_|_` y) /\ (_|_` y) (. B) -> E.x e. CH (A (. x /\ x (. B)))
33	32	ancomsd 335	. . . . . . . . 9 |- (y e. CH -> (((_|_` y) (. B /\ A (. (_|_` y)) -> E.x e. CH (A (. x /\ x (. B)))
34	33	adantl 305	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (((_|_` y) (. B /\ A (. (_|_` y)) -> E.x e. CH (A (. x /\ x (. B)))
35	25, 34	sylbid 178	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (((_|_` B) (. y /\ y (. (_|_` A)) -> E.x e. CH (A (. x /\ x (. B)))
36	35	exp 291	. . . . . 6 |- ((A e. CH /\ B e. CH) -> (y e. CH -> (((_|_` B) (. y /\ y (. (_|_` A)) -> E.x e. CH (A (. x /\ x (. B))))
37	36	r19.23adv 1286	. . . . 5 |- ((A e. CH /\ B e. CH) -> (E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)) -> E.x e. CH (A (. x /\ x (. B)))
38	19, 37	impbid 397	. . . 4 |- ((A e. CH /\ B e. CH) -> (E.x e. CH (A (. x /\ x (. B) <-> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
39	38	negbid 463	. . 3 |- ((A e. CH /\ B e. CH) -> (-. E.x e. CH (A (. x /\ x (. B) <-> -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
40	1, 39	anbi12d 476	. 2 |- ((A e. CH /\ B e. CH) -> ((A (. B /\ -. E.x e. CH (A (. x /\ x (. B)) <-> ((_|_` B) (. (_|_` A) /\ -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))))
41		cvbrt 5714	. 2 |- ((A e. CH /\ B e. CH) -> (A <o B <-> (A (. B /\ -. E.x e. CH (A (. x /\ x (. B))))
42		cvbrt 5714	. . . 4 |- (((_|_` B) e. CH /\ (_|_` A) e. CH) -> ((_|_` B) <o (_|_` A) <-> ((_|_` B) (. (_|_` A) /\ -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))))
43		choclt 5191	. . . 4 |- (B e. CH -> (_|_` B) e. CH)
44		choclt 5191	. . . 4 |- (A e. CH -> (_|_` A) e. CH)
45	42, 43, 44	syl2an 349	. . 3 |- ((B e. CH /\ A e. CH) -> ((_|_` B) <o (_|_` A) <-> ((_|_` B) (. (_|_` A) /\ -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))))
46	45	ancoms 334	. 2 |- ((A e. CH /\ B e. CH) -> ((_|_` B) <o (_|_` A) <-> ((_|_` B) (. (_|_` A) /\ -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))))
47	40, 41, 46	3bitr4d 424	1 |- ((A e. CH /\ B e. CH) -> (A <o B <-> (_|_` B) <o (_|_` A)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196   = wceq 1091   e. wcel 1092  E.wrex 1202   (. wpss 1488   class class class wbr 2054  ` cfv 2422  CHcch 4968  _|_cort 4969   <o ccv 4981

This theorem is referenced by:  cvexch 5760

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922