This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lncmp

Description: If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses lncmp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lncmp.l ⊢ ≤ = ( le ‘ 𝐾 )
lncmp.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
lncmp.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion lncmp ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 lncmp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lncmp.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lncmp.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
4 lncmp.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
5 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 )
6 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ HL )
7 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝐵 )
8 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
9 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
10 1 8 9 3 4 isline3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) )
11 6 7 10 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) )
12 5 11 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) )
13 simp3rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
14 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝐾 ∈ HL )
15 simp1l3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑌 ∈ 𝐵 )
16 simp1rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 )
17 simp3ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
18 simp3lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
19 simp3rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑝 ≠ 𝑞 )
20 14 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝐾 ∈ Lat )
21 1 9 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ 𝐵 )
22 17 21 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑝 ∈ 𝐵 )
23 simp1l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑋 ∈ 𝐵 )
24 2 8 9 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
25 14 17 18 24 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑝 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
26 25 13 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑝 ≤ 𝑋 )
27 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑋 ≤ 𝑌 )
28 1 2 20 22 23 15 26 27 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑝 ≤ 𝑌 )
29 1 9 atbase ⊢ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) → 𝑞 ∈ 𝐵 )
30 18 29 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑞 ∈ 𝐵 )
31 2 8 9 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑞 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
32 14 17 18 31 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑞 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
33 32 13 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑞 ≤ 𝑋 )
34 1 2 20 30 23 15 33 27 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑞 ≤ 𝑌 )
35 1 2 8 9 3 4 lneq2at ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ( 𝑝 ≤ 𝑌 ∧ 𝑞 ≤ 𝑌 ) ) → 𝑌 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
36 14 15 16 17 18 19 28 34 35 syl332anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑌 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
37 13 36 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ∧ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) → 𝑋 = 𝑌 )
38 37 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) → 𝑋 = 𝑌 ) )
39 38 expd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → 𝑋 = 𝑌 ) ) )
40 39 rexlimdvv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → 𝑋 = 𝑌 ) )
41 12 40 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 = 𝑌 )
42 41 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → ( 𝑋 ≤ 𝑌 → 𝑋 = 𝑌 ) )
43 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → 𝐾 ∈ HL )
44 43 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → 𝐾 ∈ Lat )
45 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → 𝑋 ∈ 𝐵 )
46 1 2 latref ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
47 44 45 46 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → 𝑋 ≤ 𝑋 )
48 breq2 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑋 ↔ 𝑋 ≤ 𝑌 ) )
49 47 48 syl5ibcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → ( 𝑋 = 𝑌 → 𝑋 ≤ 𝑌 ) )
50 42 49 impbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )