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

Metamath Proof Explorer

Theorem 2lplnja

Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj in terms of atoms). (Contributed by NM, 12-Jul-2012)

Ref Expression
Hypotheses 2lplnja.l ⊢ ≤ = ( le ‘ 𝐾 )
2lplnja.j ⊢ ∨ = ( join ‘ 𝐾 )
2lplnja.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2lplnja.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion 2lplnja ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 2lplnja.l ⊢ ≤ = ( le ‘ 𝐾 )
2 2lplnja.j ⊢ ∨ = ( join ‘ 𝐾 )
3 2lplnja.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 2lplnja.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝐾 ∈ HL )
7 6 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝐾 ∈ Lat )
8 simp121 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑃 ∈ 𝐴 )
9 simp122 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑄 ∈ 𝐴 )
10 5 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
11 6 8 9 10 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
12 simp123 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑅 ∈ 𝐴 )
13 5 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
14 12 13 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
16 7 11 14 15 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
17 simp2l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑆 ∈ 𝐴 )
18 simp2l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑇 ∈ 𝐴 )
19 5 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
20 6 17 18 19 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
21 simp2l3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑈 ∈ 𝐴 )
22 5 3 atbase ⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
23 21 22 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
24 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
25 7 20 23 24 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
26 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) )
27 7 16 25 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) )
28 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑊 ∈ 𝑉 )
29 5 4 lvolbase ⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
30 28 29 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
31 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 )
32 simp32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 )
33 5 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ≤ 𝑊 ) )
34 7 16 25 30 33 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ≤ 𝑊 ) )
35 31 32 34 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ≤ 𝑊 )
36 5 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → 𝑈 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
37 7 20 23 36 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑈 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
38 5 1 7 23 25 30 37 32 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑈 ≤ 𝑊 )
39 5 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ 𝑊 ) )
40 7 16 23 30 39 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ 𝑊 ) )
41 31 38 40 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ 𝑊 )
42 41 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ 𝑊 )
43 6 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝐾 ∈ HL )
44 6 8 9 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
45 44 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
46 12 21 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) )
47 46 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) )
48 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑃 ≠ 𝑄 )
49 48 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑃 ≠ 𝑄 )
50 simp13r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
51 50 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
52 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
53 52 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
54 simplr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
55 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
56 5 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
57 17 56 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
58 5 3 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
59 18 58 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
60 5 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
61 7 57 59 16 60 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
62 61 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
63 54 55 62 mpbi2and ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
64 63 adantr ⊢ ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
65 simpr ⊢ ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
66 5 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
67 7 20 23 16 66 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
68 67 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
69 64 65 68 mpbi2and ⊢ ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
70 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) )
71 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
72 simp2rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) )
73 simp2rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑆 ≠ 𝑇 )
74 1 2 3 3at ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≠ 𝑇 ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
75 6 70 71 72 73 74 syl32anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
76 75 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
77 69 76 mpbid ⊢ ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
78 77 eqcomd ⊢ ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
79 78 ex ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
80 79 necon3ad ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) → ¬ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
81 53 80 mpd ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ¬ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
82 1 2 3 4 lvoli2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ∈ 𝑉 )
83 45 47 49 51 81 82 syl113anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ∈ 𝑉 )
84 28 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑊 ∈ 𝑉 )
85 1 4 lvolcmp ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ 𝑊 ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) = 𝑊 ) )
86 43 83 84 85 syl3anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ 𝑊 ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) = 𝑊 ) )
87 42 86 mpbid ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) = 𝑊 )
88 5 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑈 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) )
89 7 23 25 16 88 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑈 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) )
90 37 89 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
91 90 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑈 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
92 87 91 eqbrtrrd ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑊 ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
93 5 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
94 6 17 21 93 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑆 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
95 5 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → 𝑇 ≤ ( ( 𝑆 ∨ 𝑈 ) ∨ 𝑇 ) )
96 7 94 59 95 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑇 ≤ ( ( 𝑆 ∨ 𝑈 ) ∨ 𝑇 ) )
97 2 3 hlatj32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) = ( ( 𝑆 ∨ 𝑈 ) ∨ 𝑇 ) )
98 6 17 18 21 97 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) = ( ( 𝑆 ∨ 𝑈 ) ∨ 𝑇 ) )
99 96 98 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑇 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
100 5 1 7 59 25 30 99 32 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑇 ≤ 𝑊 )
101 5 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ 𝑇 ≤ 𝑊 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 ) )
102 7 16 59 30 101 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ 𝑇 ≤ 𝑊 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 ) )
103 31 100 102 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 )
104 103 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 )
105 6 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝐾 ∈ HL )
106 44 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
107 12 18 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) )
108 107 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) )
109 48 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑃 ≠ 𝑄 )
110 50 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
111 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
112 1 2 3 4 lvoli2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ∈ 𝑉 )
113 106 108 109 110 111 112 syl113anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ∈ 𝑉 )
114 28 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑊 ∈ 𝑉 )
115 1 4 lvolcmp ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) = 𝑊 ) )
116 105 113 114 115 syl3anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) = 𝑊 ) )
117 104 116 mpbid ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) = 𝑊 )
118 5 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑇 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) )
119 7 59 25 16 118 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑇 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) )
120 99 119 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
121 120 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑇 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
122 117 121 eqbrtrrd ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑊 ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
123 92 122 pm2.61dan ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑊 ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
124 5 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
125 6 18 21 124 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
126 5 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( 𝑆 ∨ ( 𝑇 ∨ 𝑈 ) ) )
127 7 57 125 126 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑆 ≤ ( 𝑆 ∨ ( 𝑇 ∨ 𝑈 ) ) )
128 5 2 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) = ( 𝑆 ∨ ( 𝑇 ∨ 𝑈 ) ) )
129 7 57 59 23 128 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) = ( 𝑆 ∨ ( 𝑇 ∨ 𝑈 ) ) )
130 127 129 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑆 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
131 5 1 7 57 25 30 130 32 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑆 ≤ 𝑊 )
132 5 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ 𝑆 ≤ 𝑊 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 ) )
133 7 16 57 30 132 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ 𝑆 ≤ 𝑊 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 ) )
134 31 131 133 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 )
135 134 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 )
136 6 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝐾 ∈ HL )
137 44 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
138 12 17 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
139 138 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
140 48 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑃 ≠ 𝑄 )
141 50 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
142 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
143 1 2 3 4 lvoli2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )
144 137 139 140 141 142 143 syl113anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )
145 28 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑊 ∈ 𝑉 )
146 1 4 lvolcmp ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = 𝑊 ) )
147 136 144 145 146 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = 𝑊 ) )
148 135 147 mpbid ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = 𝑊 )
149 5 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑆 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) )
150 7 57 25 16 149 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( 𝑆 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) )
151 130 150 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
152 151 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
153 148 152 eqbrtrrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑊 ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
154 123 153 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → 𝑊 ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) )
155 5 1 7 27 30 35 154 latasymd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ 𝑊 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≠ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ) = 𝑊 )