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 ˙ = K
llncmp.n N = LLines K
Assertion llncmp K HL X N Y N X ˙ Y X = Y

Proof

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