Metamath Proof Explorer

Theorem 2lplnj

Description: The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012)

Ref Expression
Hypotheses 2lplnj.l ⊢ ≤ = ( le ‘ 𝐾 )
2lplnj.j ⊢ ∨ = ( join ‘ 𝐾 )
2lplnj.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
2lplnj.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion 2lplnj ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 2lplnj.l ⊢ ≤ = ( le ‘ 𝐾 )
2 2lplnj.j ⊢ ∨ = ( join ‘ 𝐾 )
3 2lplnj.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
4 2lplnj.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7 5 1 2 6 3 islpln2 ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
8 simpr ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) )
9 7 8 biimtrdi ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
10 5 1 2 6 3 islpln2 ⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ) )
11 simpr ⊢ ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
12 10 11 biimtrdi ⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑃 → ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
13 9 12 anim12d ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ) )
14 13 imp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
15 14 3adantr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
16 15 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
17 simpl33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) )
18 17 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) )
19 simp33 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) )
20 18 19 oveq12d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑋 ∨ 𝑌 ) = ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ∨ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
21 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → 𝐾 ∈ HL )
22 simp123 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → 𝑊 ∈ 𝑉 )
23 21 22 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) )
24 23 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) )
25 24 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) )
26 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
27 simp2rl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
28 simp2rr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) )
29 26 27 28 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) )
30 29 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) )
31 30 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) )
32 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑞 ≠ 𝑟 )
33 32 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑞 ≠ 𝑟 )
34 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) )
35 34 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) )
36 33 35 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ) )
37 simp1r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) )
38 simp2l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑢 ∈ ( Atoms ‘ 𝐾 ) )
39 simp2r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑣 ∈ ( Atoms ‘ 𝐾 ) )
40 37 38 39 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) )
41 simp31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑡 ≠ 𝑢 )
42 simp32 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) )
43 41 42 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ) )
44 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) )
45 44 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) )
46 breq1 ⊢ ( 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) → ( 𝑋 ≤ 𝑊 ↔ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≤ 𝑊 ) )
47 neeq1 ⊢ ( 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) → ( 𝑋 ≠ 𝑌 ↔ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ 𝑌 ) )
48 46 47 3anbi13d ⊢ ( 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ 𝑌 ) ) )
49 breq1 ⊢ ( 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) → ( 𝑌 ≤ 𝑊 ↔ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ≤ 𝑊 ) )
50 neeq2 ⊢ ( 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) → ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ 𝑌 ↔ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
51 49 50 3anbi23d ⊢ ( 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) → ( ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ 𝑌 ) ↔ ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≤ 𝑊 ∧ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ≤ 𝑊 ∧ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
52 48 51 sylan9bb ⊢ ( ( 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≤ 𝑊 ∧ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ≤ 𝑊 ∧ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
53 18 19 52 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≤ 𝑊 ∧ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ≤ 𝑊 ∧ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
54 45 53 mpbid ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≤ 𝑊 ∧ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ≤ 𝑊 ∧ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
55 1 2 6 4 2lplnja ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≤ 𝑊 ∧ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ≤ 𝑊 ∧ ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ≠ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ∨ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) = 𝑊 )
56 25 31 36 40 43 54 55 syl321anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ∨ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) = 𝑊 )
57 20 56 eqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )
58 57 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
59 58 rexlimdvv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
60 59 rexlimdva ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) → ( ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
61 60 3exp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) → ( ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) ) )
62 61 expdimp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) → ( ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) ) )
63 62 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) → ( ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
64 63 rexlimdva ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) → ( ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
65 64 impd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ 𝑋 = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑌 = ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
66 16 65 mpd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )