Metamath Proof Explorer


Theorem llncmp

Description: If two lattice lines are comparable, they are equal. (Contributed by NM, 19-Jun-2012)

Ref Expression
Hypotheses llncmp.l
|- .<_ = ( le ` K )
llncmp.n
|- N = ( LLines ` K )
Assertion llncmp
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X .<_ Y <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 llncmp.l
 |-  .<_ = ( le ` K )
2 llncmp.n
 |-  N = ( LLines ` K )
3 simp2
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> X e. N )
4 simp1
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> K e. HL )
5 eqid
 |-  ( Base ` K ) = ( Base ` K )
6 5 2 llnbase
 |-  ( X e. N -> X e. ( Base ` K ) )
7 6 3ad2ant2
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> X e. ( Base ` K ) )
8 eqid
 |-  ( 
9 eqid
 |-  ( Atoms ` K ) = ( Atoms ` K )
10 5 8 9 2 islln4
 |-  ( ( K e. HL /\ X e. ( Base ` K ) ) -> ( X e. N <-> E. p e. ( Atoms ` K ) p ( 
11 4 7 10 syl2anc
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X e. N <-> E. p e. ( Atoms ` K ) p ( 
12 3 11 mpbid
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> E. p e. ( Atoms ` K ) p ( 
13 simpr3
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  X .<_ Y )
14 hlpos
 |-  ( K e. HL -> K e. Poset )
15 14 3ad2ant1
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> K e. Poset )
16 15 adantr
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  K e. Poset )
17 7 adantr
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  X e. ( Base ` K ) )
18 simpl3
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  Y e. N )
19 5 2 llnbase
 |-  ( Y e. N -> Y e. ( Base ` K ) )
20 18 19 syl
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  Y e. ( Base ` K ) )
21 simpr1
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  p e. ( Atoms ` K ) )
22 5 9 atbase
 |-  ( p e. ( Atoms ` K ) -> p e. ( Base ` K ) )
23 21 22 syl
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  p e. ( Base ` K ) )
24 simpr2
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  p ( 
25 simpl1
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  K e. HL )
26 5 1 8 cvrle
 |-  ( ( ( K e. HL /\ p e. ( Base ` K ) /\ X e. ( Base ` K ) ) /\ p (  p .<_ X )
27 25 23 17 24 26 syl31anc
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  p .<_ X )
28 5 1 postr
 |-  ( ( K e. Poset /\ ( p e. ( Base ` K ) /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) ) -> ( ( p .<_ X /\ X .<_ Y ) -> p .<_ Y ) )
29 16 23 17 20 28 syl13anc
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  ( ( p .<_ X /\ X .<_ Y ) -> p .<_ Y ) )
30 27 13 29 mp2and
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  p .<_ Y )
31 1 8 9 2 atcvrlln2
 |-  ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ Y e. N ) /\ p .<_ Y ) -> p ( 
32 25 21 18 30 31 syl31anc
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  p ( 
33 5 1 8 cvrcmp
 |-  ( ( K e. Poset /\ ( X e. ( Base ` K ) /\ Y e. ( Base ` K ) /\ p e. ( Base ` K ) ) /\ ( p (  ( X .<_ Y <-> X = Y ) )
34 16 17 20 23 24 32 33 syl132anc
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  ( X .<_ Y <-> X = Y ) )
35 13 34 mpbid
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p (  X = Y )
36 35 3exp2
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( p e. ( Atoms ` K ) -> ( p (  ( X .<_ Y -> X = Y ) ) ) )
37 36 rexlimdv
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( E. p e. ( Atoms ` K ) p (  ( X .<_ Y -> X = Y ) ) )
38 12 37 mpd
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X .<_ Y -> X = Y ) )
39 5 1 posref
 |-  ( ( K e. Poset /\ X e. ( Base ` K ) ) -> X .<_ X )
40 15 7 39 syl2anc
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> X .<_ X )
41 breq2
 |-  ( X = Y -> ( X .<_ X <-> X .<_ Y ) )
42 40 41 syl5ibcom
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X = Y -> X .<_ Y ) )
43 38 42 impbid
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X .<_ Y <-> X = Y ) )