Theorem lneq2at

Description: A line equals the join of any two of its distinct points (atoms). (Contributed by NM, 29-Apr-2012)

	Ref	Expression
Hypotheses	lneq2at.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lneq2at.l	⊢ ≤ = ( le ‘ 𝐾 )
	lneq2at.j	⊢ ∨ = ( join ‘ 𝐾 )
	lneq2at.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lneq2at.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
	lneq2at.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	lneq2at	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝑋 = ( 𝑃 ∨ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		lneq2at.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lneq2at.l	⊢ ≤ = ( le ‘ 𝐾 )
3		lneq2at.j	⊢ ∨ = ( join ‘ 𝐾 )
4		lneq2at.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		lneq2at.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
6		lneq2at.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
7		simp11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
8		simp12	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
9	7 8	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) )
10		simp13	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 )
11	1 3 4 5 6	isline3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) )
12	11	biimpd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) )
13	9 10 12	sylc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) )
14		simp3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → 𝑋 = ( 𝑟 ∨ 𝑠 ) )
15		simp111	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → 𝐾 ∈ HL )
16		simp121	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → 𝑃 ∈ 𝐴 )
17		simp122	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → 𝑄 ∈ 𝐴 )
18	16 17	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
19		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) )
20	15 18 19	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) )
21		simp123	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → 𝑃 ≠ 𝑄 )
22	20 21	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) )
23	7	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
24		simp21	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐴 )
25	1 4	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
26	24 25	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐵 )
27		simp22	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐴 )
28	1 4	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
29	27 28	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐵 )
30	26 29 8	3jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ( 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
31	23 30	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) )
32		simp3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) )
33	1 2 3	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑋 ) )
34	33	biimpd	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) → ( 𝑃 ∨ 𝑄 ) ≤ 𝑋 ) )
35	31 32 34	sylc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ 𝑋 )
36	35	3ad2ant1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → ( 𝑃 ∨ 𝑄 ) ≤ 𝑋 )
37	36 14	breqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑟 ∨ 𝑠 ) )
38		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝐾 ∈ HL )
39		simpl2l	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ 𝐴 )
40		simpl2r	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ 𝐴 )
41		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ≠ 𝑄 )
42		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) )
43	2 3 4	ps-1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑟 ∨ 𝑠 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ) )
44	38 39 40 41 42 43	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑟 ∨ 𝑠 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ) )
45	44	biimpd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑟 ∨ 𝑠 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ) )
46	22 37 45	sylc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) )
47	14 46	eqtr4d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) ) → 𝑋 = ( 𝑃 ∨ 𝑄 ) )
48	47	3exp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) → 𝑋 = ( 𝑃 ∨ 𝑄 ) ) ) )
49	48	rexlimdvv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ∨ 𝑠 ) ) → 𝑋 = ( 𝑃 ∨ 𝑄 ) ) )
50	13 49	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝑋 = ( 𝑃 ∨ 𝑄 ) )