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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝑀 ‘ 𝑌 ) ∈ 𝑁 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )