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 ) )