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

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ) → 𝑋 = ( 𝑃 ∨ 𝑄 ) )