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

Metamath Proof Explorer

Theorem dalawlem1

Description: Lemma for dalaw . Special case of dath2 , where C is replaced by ( ( P .\/ S ) ./\ ( Q .\/ T ) ) . The remaining lemmas will eliminate the conditions on the atoms imposed by dath2 . (Contributed by NM, 6-Oct-2012)

Ref Expression
Hypotheses dalawlem.l ⊢ ≤ = ( le ‘ 𝐾 )
dalawlem.j ⊢ ∨ = ( join ‘ 𝐾 )
dalawlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
dalawlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dalawlem.o ⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
Assertion dalawlem1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 dalawlem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dalawlem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dalawlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dalawlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dalawlem.o ⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
6 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → 𝐾 ∈ HL )
7 6 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → 𝐾 ∈ Lat )
8 simp121 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → 𝑃 ∈ 𝐴 )
9 simp131 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → 𝑆 ∈ 𝐴 )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
12 6 8 9 11 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
13 simp122 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → 𝑄 ∈ 𝐴 )
14 simp132 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → 𝑇 ∈ 𝐴 )
15 10 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
16 6 13 14 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
17 10 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
18 7 12 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
19 6 18 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) )
20 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
21 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) )
22 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 )
23 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 )
24 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) )
25 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) )
26 10 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑆 ) )
27 7 12 16 26 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑆 ) )
28 10 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑇 ) )
29 7 12 16 28 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑇 ) )
30 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) )
31 27 29 30 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑆 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) )
32 eqid ⊢ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) )
33 eqid ⊢ ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) = ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) )
34 eqid ⊢ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) )
35 10 1 2 4 3 5 32 33 34 dath2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑆 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )
36 19 20 21 22 23 24 25 31 35 syl323anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )