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

Metamath Proof Explorer

Theorem 2llnjN

Description: The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnj.l ⊢ ≤ = ( le ‘ 𝐾 )
2llnj.j ⊢ ∨ = ( join ‘ 𝐾 )
2llnj.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
2llnj.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion 2llnjN ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 2llnj.l ⊢ ≤ = ( le ‘ 𝐾 )
2 2llnj.j ⊢ ∨ = ( join ‘ 𝐾 )
3 2llnj.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
4 2llnj.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7 5 2 6 3 islln2 ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ) )
8 simpr ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) )
9 7 8 biimtrdi ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) )
10 5 2 6 3 islln2 ⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑁 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) )
11 simpr ⊢ ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) )
12 10 11 biimtrdi ⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑁 → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) )
13 9 12 anim12d ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) )
14 13 imp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) )
15 14 3adantr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) )
16 15 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) )
17 simp2rr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑋 = ( 𝑞 ∨ 𝑟 ) )
18 simp3rr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑌 = ( 𝑠 ∨ 𝑡 ) )
19 17 18 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ∨ 𝑌 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) )
20 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) )
21 breq1 ⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( 𝑋 ≤ 𝑊 ↔ ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ) )
22 neeq1 ⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( 𝑋 ≠ 𝑌 ↔ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) )
23 21 22 3anbi13d ⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) ) )
24 breq1 ⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( 𝑌 ≤ 𝑊 ↔ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ) )
25 neeq2 ⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ↔ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) )
26 24 25 3anbi23d ⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) )
27 23 26 sylan9bb ⊢ ( ( 𝑋 = ( 𝑞 ∨ 𝑟 ) ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) )
28 17 18 27 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) )
29 20 28 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) )
30 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝐾 ∈ HL )
31 simp123 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑊 ∈ 𝑃 )
32 simp2ll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
33 simp2lr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
34 simp2rl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑞 ≠ 𝑟 )
35 simp3ll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) )
36 simp3lr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) )
37 simp3rl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑠 ≠ 𝑡 )
38 1 2 6 3 4 2llnjaN ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ≠ 𝑟 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ≠ 𝑡 ) ) ∧ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 )
39 38 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ≠ 𝑟 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ≠ 𝑡 ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 ) )
40 30 31 32 33 34 35 36 37 39 syl233anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 ) )
41 29 40 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 )
42 19 41 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )
43 42 3exp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
44 43 3impib ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
45 44 expd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
46 45 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
47 46 3exp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) ) )
48 47 rexlimdvv ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
49 48 impd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
50 16 49 mpd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )