Metamath Proof Explorer

Theorem paddasslem15

Description: Lemma for paddass . Use elpaddn0 to eliminate y and z from paddasslem14 . (Contributed by NM, 11-Jan-2012)

Ref Expression
Hypotheses paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddasslem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddasslem15 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )

Proof

Step Hyp Ref Expression
1 paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddasslem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 simpr2r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝑟 ∈ ( 𝑌 + 𝑍 ) )
6 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝐾 ∈ HL )
7 6 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝐾 ∈ Lat )
8 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝑌 ⊆ 𝐴 )
9 simpl23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝑍 ⊆ 𝐴 )
10 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) )
11 1 2 3 4 elpaddn0 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) → ( 𝑟 ∈ ( 𝑌 + 𝑍 ) ↔ ( 𝑟 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝑌 ∃ 𝑧 ∈ 𝑍 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) )
12 7 8 9 10 11 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → ( 𝑟 ∈ ( 𝑌 + 𝑍 ) ↔ ( 𝑟 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝑌 ∃ 𝑧 ∈ 𝑍 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) )
13 5 12 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → ( 𝑟 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝑌 ∃ 𝑧 ∈ 𝑍 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) )
14 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝐾 ∈ HL )
15 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) )
16 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ 𝐴 )
17 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑟 ∈ 𝐴 )
18 16 17 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) )
19 simp22l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑥 ∈ 𝑋 )
20 simp32l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑦 ∈ 𝑌 )
21 simp32r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑧 ∈ 𝑍 )
22 19 20 21 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) )
23 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) )
24 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) )
25 23 24 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) )
26 1 2 3 4 paddasslem14 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
27 14 15 18 22 25 26 syl32anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
28 27 3expia ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → ( ( 𝑟 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
29 28 3expd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → ( 𝑟 ∈ 𝐴 → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → ( 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
30 29 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → ( 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) )
31 30 rexlimdvv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ∧ 𝑟 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝑌 ∃ 𝑧 ∈ 𝑍 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
32 31 expimpd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → ( ( 𝑟 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝑌 ∃ 𝑧 ∈ 𝑍 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
33 13 32 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )