Theorem cvcon3t 10121

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 9341	. . 3 |- ((A e. CH /\ B e. CH) -> (A (. B <-> (_|_` B) (. (_|_` A)))
2		chpsscon3t 9341	. . . . . . . . 9 |- ((A e. CH /\ x e. CH) -> (A (. x <-> (_|_` x) (. (_|_` A)))
3	2	adantlr 393	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (A (. x <-> (_|_` x) (. (_|_` A)))
4		chpsscon3t 9341	. . . . . . . . . 10 |- ((x e. CH /\ B e. CH) -> (x (. B <-> (_|_` B) (. (_|_` x)))
5	4	ancoms 436	. . . . . . . . 9 |- ((B e. CH /\ x e. CH) -> (x (. B <-> (_|_` B) (. (_|_` x)))
6	5	adantll 392	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (x (. B <-> (_|_` B) (. (_|_` x)))
7	3, 6	anbi12d 626	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> ((A (. x /\ x (. B) <-> ((_|_` x) (. (_|_` A) /\ (_|_` B) (. (_|_` x))))
8		psseq2 2126	. . . . . . . . . . . . 13 |- (y = (_|_` x) -> ((_|_` B) (. y <-> (_|_` B) (. (_|_` x)))
9		psseq1 2125	. . . . . . . . . . . . 13 |- (y = (_|_` x) -> (y (. (_|_` A) <-> (_|_` x) (. (_|_` A)))
10	8, 9	anbi12d 626	. . . . . . . . . . . 12 |- (y = (_|_` x) -> (((_|_` B) (. y /\ y (. (_|_` A)) <-> ((_|_` B) (. (_|_` x) /\ (_|_` x) (. (_|_` A))))
11	10	rcla4ev 1868	. . . . . . . . . . 11 |- (((_|_` x) e. CH /\ ((_|_` B) (. (_|_` x) /\ (_|_` x) (. (_|_` A))) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))
12		chocclt 9100	. . . . . . . . . . 11 |- (x e. CH -> (_|_` x) e. CH)
13	11, 12	sylan 448	. . . . . . . . . 10 |- ((x e. CH /\ ((_|_` B) (. (_|_` x) /\ (_|_` x) (. (_|_` A))) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))
14	13	ex 373	. . . . . . . . 9 |- (x e. CH -> (((_|_` B) (. (_|_` x) /\ (_|_` x) (. (_|_` A)) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
15	14	ancomsd 437	. . . . . . . 8 |- (x e. CH -> (((_|_` x) (. (_|_` A) /\ (_|_` B) (. (_|_` x)) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
16	15	adantl 388	. . . . . . 7 |- (((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 203	. . . . . 6 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> ((A (. x /\ x (. B) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
18	17	r19.23adva 1739	. . . . 5 |- ((A e. CH /\ B e. CH) -> (E.x e. CH (A (. x /\ x (. B) -> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
19		chpsscon1t 9342	. . . . . . . . 9 |- ((B e. CH /\ y e. CH) -> ((_|_` B) (. y <-> (_|_` y) (. B))
20	19	adantll 392	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((_|_` B) (. y <-> (_|_` y) (. B))
21		chpsscon2t 9343	. . . . . . . . . 10 |- ((y e. CH /\ A e. CH) -> (y (. (_|_` A) <-> A (. (_|_` y)))
22	21	ancoms 436	. . . . . . . . 9 |- ((A e. CH /\ y e. CH) -> (y (. (_|_` A) <-> A (. (_|_` y)))
23	22	adantlr 393	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (y (. (_|_` A) <-> A (. (_|_` y)))
24	20, 23	anbi12d 626	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (((_|_` B) (. y /\ y (. (_|_` A)) <-> ((_|_` y) (. B /\ A (. (_|_` y))))
25		psseq2 2126	. . . . . . . . . . . . 13 |- (x = (_|_` y) -> (A (. x <-> A (. (_|_` y)))
26		psseq1 2125	. . . . . . . . . . . . 13 |- (x = (_|_` y) -> (x (. B <-> (_|_` y) (. B))
27	25, 26	anbi12d 626	. . . . . . . . . . . 12 |- (x = (_|_` y) -> ((A (. x /\ x (. B) <-> (A (. (_|_` y) /\ (_|_` y) (. B)))
28	27	rcla4ev 1868	. . . . . . . . . . 11 |- (((_|_` y) e. CH /\ (A (. (_|_` y) /\ (_|_` y) (. B)) -> E.x e. CH (A (. x /\ x (. B))
29		chocclt 9100	. . . . . . . . . . 11 |- (y e. CH -> (_|_` y) e. CH)
30	28, 29	sylan 448	. . . . . . . . . 10 |- ((y e. CH /\ (A (. (_|_` y) /\ (_|_` y) (. B)) -> E.x e. CH (A (. x /\ x (. B))
31	30	ex 373	. . . . . . . . 9 |- (y e. CH -> ((A (. (_|_` y) /\ (_|_` y) (. B) -> E.x e. CH (A (. x /\ x (. B)))
32	31	ancomsd 437	. . . . . . . 8 |- (y e. CH -> (((_|_` y) (. B /\ A (. (_|_` y)) -> E.x e. CH (A (. x /\ x (. B)))
33	32	adantl 388	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (((_|_` y) (. B /\ A (. (_|_` y)) -> E.x e. CH (A (. x /\ x (. B)))
34	24, 33	sylbid 203	. . . . . 6 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (((_|_` B) (. y /\ y (. (_|_` A)) -> E.x e. CH (A (. x /\ x (. B)))
35	34	r19.23adva 1739	. . . . 5 |- ((A e. CH /\ B e. CH) -> (E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)) -> E.x e. CH (A (. x /\ x (. B)))
36	18, 35	impbid 514	. . . 4 |- ((A e. CH /\ B e. CH) -> (E.x e. CH (A (. x /\ x (. B) <-> E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
37	36	negbid 609	. . 3 |- ((A e. CH /\ B e. CH) -> (-. E.x e. CH (A (. x /\ x (. B) <-> -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A))))
38	1, 37	anbi12d 626	. 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)))))
39		cvbrt 10119	. 2 |- ((A e. CH /\ B e. CH) -> (A <o B <-> (A (. B /\ -. E.x e. CH (A (. x /\ x (. B))))
40		cvbrt 10119	. . . 4 |- (((_|_` B) e. CH /\ (_|_` A) e. CH) -> ((_|_` B) <o (_|_` A) <-> ((_|_` B) (. (_|_` A) /\ -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))))
41		chocclt 9100	. . . 4 |- (B e. CH -> (_|_` B) e. CH)
42		chocclt 9100	. . . 4 |- (A e. CH -> (_|_` A) e. CH)
43	40, 41, 42	syl2an 454	. . 3 |- ((B e. CH /\ A e. CH) -> ((_|_` B) <o (_|_` A) <-> ((_|_` B) (. (_|_` A) /\ -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))))
44	43	ancoms 436	. 2 |- ((A e. CH /\ B e. CH) -> ((_|_` B) <o (_|_` A) <-> ((_|_` B) (. (_|_` A) /\ -. E.y e. CH ((_|_` B) (. y /\ y (. (_|_` A)))))
45	38, 39, 44	3bitr4d 548	1 |- ((A e. CH /\ B e. CH) -> (A <o B <-> (_|_` B) <o (_|_` A)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wrex 1638   (. wpss 2038   class class class wbr 2609  ` cfv 3172  CHcch 8737  _|_cort 8738   <o ccv 8773

This theorem is referenced by:  cvdmdt 10172  cvexch 10204

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-reg 4565  ax-inf2 4597  ax-ac 4716  ax-hilex 8790  ax-hfvadd 8791  ax-hvcom 8792  ax-hvass 8793  ax-hv0cl 8794  ax-hvaddid 8795  ax-hfvmul 8796  ax-hvmulid 8797  ax-hvmulass 8798  ax-hvdistr1 8799  ax-hvdistr2 8800  ax-hvmul0 8801  ax-hfi 8867  ax-his1 8870  ax-his2 8871  ax-his3 8872  ax-his4 8873  ax-hcompl 8992

This theorem depends on definitions:  df-bi 147