Metamath Proof Explorer

Theorem cvrcon3b

Description: Contraposition law for the covers relation. ( cvcon3 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses cvrcon3b.b 
|- B = ( Base ` K )
cvrcon3b.o 
|- ._|_ = ( oc ` K )
cvrcon3b.c 
|- C = (
Assertion cvrcon3b 
|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( ._|_ ` Y ) C ( ._|_ ` X ) ) )

Proof

Step Hyp Ref Expression
1 cvrcon3b.b 
 |-  B = ( Base ` K )
2 cvrcon3b.o 
 |-  ._|_ = ( oc ` K )
3 cvrcon3b.c 
 |-  C = (
4 eqid 
 |-  ( lt ` K ) = ( lt ` K )
5 1 4 2 opltcon3b 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X ( lt ` K ) Y <-> ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` X ) ) )
6 simpl1 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> K e. OP )
7 simpl2 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> X e. B )
8 simpr 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> x e. B )
9 1 4 2 opltcon3b 
 |-  ( ( K e. OP /\ X e. B /\ x e. B ) -> ( X ( lt ` K ) x <-> ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> ( X ( lt ` K ) x <-> ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) ) )
11 simpl3 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> Y e. B )
12 1 4 2 opltcon3b 
 |-  ( ( K e. OP /\ x e. B /\ Y e. B ) -> ( x ( lt ` K ) Y <-> ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) ) )
13 6 8 11 12 syl3anc 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> ( x ( lt ` K ) Y <-> ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) ) )
14 10 13 anbi12d 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> ( ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) <-> ( ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) /\ ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) ) ) )
15 1 2 opoccl 
 |-  ( ( K e. OP /\ x e. B ) -> ( ._|_ ` x ) e. B )
16 15 3ad2antl1 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> ( ._|_ ` x ) e. B )
17 breq2 
 |-  ( y = ( ._|_ ` x ) -> ( ( ._|_ ` Y ) ( lt ` K ) y <-> ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) ) )
18 breq1 
 |-  ( y = ( ._|_ ` x ) -> ( y ( lt ` K ) ( ._|_ ` X ) <-> ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) ) )
19 17 18 anbi12d 
 |-  ( y = ( ._|_ ` x ) -> ( ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) <-> ( ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) /\ ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) ) ) )
20 19 rspcev 
 |-  ( ( ( ._|_ ` x ) e. B /\ ( ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) /\ ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) ) ) -> E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) )
21 20 ex 
 |-  ( ( ._|_ ` x ) e. B -> ( ( ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) /\ ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) ) -> E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) )
22 16 21 syl 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> ( ( ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) /\ ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) ) -> E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) )
23 22 ancomsd 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> ( ( ( ._|_ ` x ) ( lt ` K ) ( ._|_ ` X ) /\ ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` x ) ) -> E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) )
24 14 23 sylbid 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ x e. B ) -> ( ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) -> E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) )
25 24 rexlimdva 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) -> E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) )
26 simpl1 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> K e. OP )
27 simpl3 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> Y e. B )
28 simpr 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> y e. B )
29 1 4 2 opltcon1b 
 |-  ( ( K e. OP /\ Y e. B /\ y e. B ) -> ( ( ._|_ ` Y ) ( lt ` K ) y <-> ( ._|_ ` y ) ( lt ` K ) Y ) )
30 26 27 28 29 syl3anc 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> ( ( ._|_ ` Y ) ( lt ` K ) y <-> ( ._|_ ` y ) ( lt ` K ) Y ) )
31 simpl2 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> X e. B )
32 1 4 2 opltcon2b 
 |-  ( ( K e. OP /\ y e. B /\ X e. B ) -> ( y ( lt ` K ) ( ._|_ ` X ) <-> X ( lt ` K ) ( ._|_ ` y ) ) )
33 26 28 31 32 syl3anc 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> ( y ( lt ` K ) ( ._|_ ` X ) <-> X ( lt ` K ) ( ._|_ ` y ) ) )
34 30 33 anbi12d 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> ( ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) <-> ( ( ._|_ ` y ) ( lt ` K ) Y /\ X ( lt ` K ) ( ._|_ ` y ) ) ) )
35 1 2 opoccl 
 |-  ( ( K e. OP /\ y e. B ) -> ( ._|_ ` y ) e. B )
36 35 3ad2antl1 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> ( ._|_ ` y ) e. B )
37 breq2 
 |-  ( x = ( ._|_ ` y ) -> ( X ( lt ` K ) x <-> X ( lt ` K ) ( ._|_ ` y ) ) )
38 breq1 
 |-  ( x = ( ._|_ ` y ) -> ( x ( lt ` K ) Y <-> ( ._|_ ` y ) ( lt ` K ) Y ) )
39 37 38 anbi12d 
 |-  ( x = ( ._|_ ` y ) -> ( ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) <-> ( X ( lt ` K ) ( ._|_ ` y ) /\ ( ._|_ ` y ) ( lt ` K ) Y ) ) )
40 39 rspcev 
 |-  ( ( ( ._|_ ` y ) e. B /\ ( X ( lt ` K ) ( ._|_ ` y ) /\ ( ._|_ ` y ) ( lt ` K ) Y ) ) -> E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) )
41 40 ex 
 |-  ( ( ._|_ ` y ) e. B -> ( ( X ( lt ` K ) ( ._|_ ` y ) /\ ( ._|_ ` y ) ( lt ` K ) Y ) -> E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) ) )
42 36 41 syl 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> ( ( X ( lt ` K ) ( ._|_ ` y ) /\ ( ._|_ ` y ) ( lt ` K ) Y ) -> E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) ) )
43 42 ancomsd 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> ( ( ( ._|_ ` y ) ( lt ` K ) Y /\ X ( lt ` K ) ( ._|_ ` y ) ) -> E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) ) )
44 34 43 sylbid 
 |-  ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ y e. B ) -> ( ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) -> E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) ) )
45 44 rexlimdva 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) -> E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) ) )
46 25 45 impbid 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) <-> E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) )
47 46 notbid 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( -. E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) <-> -. E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) )
48 5 47 anbi12d 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( X ( lt ` K ) Y /\ -. E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) ) <-> ( ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` X ) /\ -. E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) ) )
49 1 4 3 cvrval 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ( lt ` K ) Y /\ -. E. x e. B ( X ( lt ` K ) x /\ x ( lt ` K ) Y ) ) ) )
50 simp1 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> K e. OP )
51 1 2 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
52 51 3adant2 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
53 1 2 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
54 53 3adant3 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
55 1 4 3 cvrval 
 |-  ( ( K e. OP /\ ( ._|_ ` Y ) e. B /\ ( ._|_ ` X ) e. B ) -> ( ( ._|_ ` Y ) C ( ._|_ ` X ) <-> ( ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` X ) /\ -. E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) ) )
56 50 52 54 55 syl3anc 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) C ( ._|_ ` X ) <-> ( ( ._|_ ` Y ) ( lt ` K ) ( ._|_ ` X ) /\ -. E. y e. B ( ( ._|_ ` Y ) ( lt ` K ) y /\ y ( lt ` K ) ( ._|_ ` X ) ) ) ) )
57 48 49 56 3bitr4d 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( ._|_ ` Y ) C ( ._|_ ` X ) ) )