Metamath Proof Explorer

Theorem cvcon3

Description: Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvcon3 
|- ( ( A e. CH /\ B e. CH ) -> ( A  ( _|_ ` B )

Proof

Step Hyp Ref Expression
1 chpsscon3 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C. B <-> ( _|_ ` B ) C. ( _|_ ` A ) ) )
2 chpsscon3 
 |-  ( ( A e. CH /\ x e. CH ) -> ( A C. x <-> ( _|_ ` x ) C. ( _|_ ` A ) ) )
3 2 adantlr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( A C. x <-> ( _|_ ` x ) C. ( _|_ ` A ) ) )
4 chpsscon3 
 |-  ( ( x e. CH /\ B e. CH ) -> ( x C. B <-> ( _|_ ` B ) C. ( _|_ ` x ) ) )
5 4 ancoms 
 |-  ( ( B e. CH /\ x e. CH ) -> ( x C. B <-> ( _|_ ` B ) C. ( _|_ ` x ) ) )
6 5 adantll 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( x C. B <-> ( _|_ ` B ) C. ( _|_ ` x ) ) )
7 3 6 anbi12d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( A C. x /\ x C. B ) <-> ( ( _|_ ` x ) C. ( _|_ ` A ) /\ ( _|_ ` B ) C. ( _|_ ` x ) ) ) )
8 choccl 
 |-  ( x e. CH -> ( _|_ ` x ) e. CH )
9 psseq2 
 |-  ( y = ( _|_ ` x ) -> ( ( _|_ ` B ) C. y <-> ( _|_ ` B ) C. ( _|_ ` x ) ) )
10 psseq1 
 |-  ( y = ( _|_ ` x ) -> ( y C. ( _|_ ` A ) <-> ( _|_ ` x ) C. ( _|_ ` A ) ) )
11 9 10 anbi12d 
 |-  ( y = ( _|_ ` x ) -> ( ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) <-> ( ( _|_ ` B ) C. ( _|_ ` x ) /\ ( _|_ ` x ) C. ( _|_ ` A ) ) ) )
12 11 rspcev 
 |-  ( ( ( _|_ ` x ) e. CH /\ ( ( _|_ ` B ) C. ( _|_ ` x ) /\ ( _|_ ` x ) C. ( _|_ ` A ) ) ) -> E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) )
13 8 12 sylan 
 |-  ( ( x e. CH /\ ( ( _|_ ` B ) C. ( _|_ ` x ) /\ ( _|_ ` x ) C. ( _|_ ` A ) ) ) -> E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) )
14 13 ex 
 |-  ( x e. CH -> ( ( ( _|_ ` B ) C. ( _|_ ` x ) /\ ( _|_ ` x ) C. ( _|_ ` A ) ) -> E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) )
15 14 ancomsd 
 |-  ( x e. CH -> ( ( ( _|_ ` x ) C. ( _|_ ` A ) /\ ( _|_ ` B ) C. ( _|_ ` x ) ) -> E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) )
16 15 adantl 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( ( _|_ ` x ) C. ( _|_ ` A ) /\ ( _|_ ` B ) C. ( _|_ ` x ) ) -> E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) )
17 7 16 sylbid 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( A C. x /\ x C. B ) -> E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) )
18 17 rexlimdva 
 |-  ( ( A e. CH /\ B e. CH ) -> ( E. x e. CH ( A C. x /\ x C. B ) -> E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) )
19 chpsscon1 
 |-  ( ( B e. CH /\ y e. CH ) -> ( ( _|_ ` B ) C. y <-> ( _|_ ` y ) C. B ) )
20 19 adantll 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( _|_ ` B ) C. y <-> ( _|_ ` y ) C. B ) )
21 chpsscon2 
 |-  ( ( y e. CH /\ A e. CH ) -> ( y C. ( _|_ ` A ) <-> A C. ( _|_ ` y ) ) )
22 21 ancoms 
 |-  ( ( A e. CH /\ y e. CH ) -> ( y C. ( _|_ ` A ) <-> A C. ( _|_ ` y ) ) )
23 22 adantlr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( y C. ( _|_ ` A ) <-> A C. ( _|_ ` y ) ) )
24 20 23 anbi12d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) <-> ( ( _|_ ` y ) C. B /\ A C. ( _|_ ` y ) ) ) )
25 choccl 
 |-  ( y e. CH -> ( _|_ ` y ) e. CH )
26 psseq2 
 |-  ( x = ( _|_ ` y ) -> ( A C. x <-> A C. ( _|_ ` y ) ) )
27 psseq1 
 |-  ( x = ( _|_ ` y ) -> ( x C. B <-> ( _|_ ` y ) C. B ) )
28 26 27 anbi12d 
 |-  ( x = ( _|_ ` y ) -> ( ( A C. x /\ x C. B ) <-> ( A C. ( _|_ ` y ) /\ ( _|_ ` y ) C. B ) ) )
29 28 rspcev 
 |-  ( ( ( _|_ ` y ) e. CH /\ ( A C. ( _|_ ` y ) /\ ( _|_ ` y ) C. B ) ) -> E. x e. CH ( A C. x /\ x C. B ) )
30 25 29 sylan 
 |-  ( ( y e. CH /\ ( A C. ( _|_ ` y ) /\ ( _|_ ` y ) C. B ) ) -> E. x e. CH ( A C. x /\ x C. B ) )
31 30 ex 
 |-  ( y e. CH -> ( ( A C. ( _|_ ` y ) /\ ( _|_ ` y ) C. B ) -> E. x e. CH ( A C. x /\ x C. B ) ) )
32 31 ancomsd 
 |-  ( y e. CH -> ( ( ( _|_ ` y ) C. B /\ A C. ( _|_ ` y ) ) -> E. x e. CH ( A C. x /\ x C. B ) ) )
33 32 adantl 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( _|_ ` y ) C. B /\ A C. ( _|_ ` y ) ) -> E. x e. CH ( A C. x /\ x C. B ) ) )
34 24 33 sylbid 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) -> E. x e. CH ( A C. x /\ x C. B ) ) )
35 34 rexlimdva 
 |-  ( ( A e. CH /\ B e. CH ) -> ( E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) -> E. x e. CH ( A C. x /\ x C. B ) ) )
36 18 35 impbid 
 |-  ( ( A e. CH /\ B e. CH ) -> ( E. x e. CH ( A C. x /\ x C. B ) <-> E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) )
37 36 notbid 
 |-  ( ( A e. CH /\ B e. CH ) -> ( -. E. x e. CH ( A C. x /\ x C. B ) <-> -. E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) )
38 1 37 anbi12d 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) <-> ( ( _|_ ` B ) C. ( _|_ ` A ) /\ -. E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) ) )
39 cvbr 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) ) )
40 choccl 
 |-  ( B e. CH -> ( _|_ ` B ) e. CH )
41 choccl 
 |-  ( A e. CH -> ( _|_ ` A ) e. CH )
42 cvbr 
 |-  ( ( ( _|_ ` B ) e. CH /\ ( _|_ ` A ) e. CH ) -> ( ( _|_ ` B )  ( ( _|_ ` B ) C. ( _|_ ` A ) /\ -. E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) ) )
43 40 41 42 syl2anr 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( _|_ ` B )  ( ( _|_ ` B ) C. ( _|_ ` A ) /\ -. E. y e. CH ( ( _|_ ` B ) C. y /\ y C. ( _|_ ` A ) ) ) ) )
44 38 39 43 3bitr4d 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  ( _|_ ` B )