Metamath Proof Explorer

Theorem cvrcmp2

Description: If two lattice elements covered by a third are comparable, then they are equal. (Contributed by NM, 20-Jun-2012)

Ref Expression
Hypotheses cvrcmp.b 
|- B = ( Base ` K )
cvrcmp.l 
|- .<_ = ( le ` K )
cvrcmp.c 
|- C = (
Assertion cvrcmp2 
|- ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( X .<_ Y <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 cvrcmp.b 
 |-  B = ( Base ` K )
2 cvrcmp.l 
 |-  .<_ = ( le ` K )
3 cvrcmp.c 
 |-  C = (
4 opposet 
 |-  ( K e. OP -> K e. Poset )
5 4 3ad2ant1 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> K e. Poset )
6 simp1 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> K e. OP )
7 simp22 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> Y e. B )
8 eqid 
 |-  ( oc ` K ) = ( oc ` K )
9 1 8 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
10 6 7 9 syl2anc 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( ( oc ` K ) ` Y ) e. B )
11 simp21 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> X e. B )
12 1 8 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
13 6 11 12 syl2anc 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( ( oc ` K ) ` X ) e. B )
14 simp23 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> Z e. B )
15 1 8 opoccl 
 |-  ( ( K e. OP /\ Z e. B ) -> ( ( oc ` K ) ` Z ) e. B )
16 6 14 15 syl2anc 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( ( oc ` K ) ` Z ) e. B )
17 1 8 3 cvrcon3b 
 |-  ( ( K e. OP /\ X e. B /\ Z e. B ) -> ( X C Z <-> ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` X ) ) )
18 17 3adant3r2 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Z <-> ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` X ) ) )
19 1 8 3 cvrcon3b 
 |-  ( ( K e. OP /\ Y e. B /\ Z e. B ) -> ( Y C Z <-> ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` Y ) ) )
20 19 3adant3r1 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y C Z <-> ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` Y ) ) )
21 18 20 anbi12d 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X C Z /\ Y C Z ) <-> ( ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` X ) /\ ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` Y ) ) ) )
22 21 biimp3a 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` X ) /\ ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` Y ) ) )
23 22 ancomd 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` Y ) /\ ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` X ) ) )
24 1 2 3 cvrcmp 
 |-  ( ( K e. Poset /\ ( ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) /\ ( ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` Y ) /\ ( ( oc ` K ) ` Z ) C ( ( oc ` K ) ` X ) ) ) -> ( ( ( oc ` K ) ` Y ) .<_ ( ( oc ` K ) ` X ) <-> ( ( oc ` K ) ` Y ) = ( ( oc ` K ) ` X ) ) )
25 5 10 13 16 23 24 syl131anc 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( ( ( oc ` K ) ` Y ) .<_ ( ( oc ` K ) ` X ) <-> ( ( oc ` K ) ` Y ) = ( ( oc ` K ) ` X ) ) )
26 1 2 8 oplecon3b 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ( oc ` K ) ` Y ) .<_ ( ( oc ` K ) ` X ) ) )
27 6 11 7 26 syl3anc 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( X .<_ Y <-> ( ( oc ` K ) ` Y ) .<_ ( ( oc ` K ) ` X ) ) )
28 1 8 opcon3b 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = Y <-> ( ( oc ` K ) ` Y ) = ( ( oc ` K ) ` X ) ) )
29 6 11 7 28 syl3anc 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( X = Y <-> ( ( oc ` K ) ` Y ) = ( ( oc ` K ) ` X ) ) )
30 25 27 29 3bitr4d 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( X .<_ Y <-> X = Y ) )