Metamath Proof Explorer

Theorem cdleme22eALTN

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 4th line on p. 115. F , N , O represent f(z), f_z(s), f_z(t) respectively. When t \/ v = p \/ q, f_z(s) <_ f_z(t) \/ v. (Contributed by NM, 6-Dec-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme22.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme22.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme22.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme22.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme22.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme22eALT.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme22eALT.f ⊢ 𝐹 = ( ( 𝑦 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑦 ) ∧ 𝑊 ) ) )
cdleme22eALT.g ⊢ 𝐺 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
cdleme22eALT.n ⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) )
cdleme22eALT.o ⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
Assertion cdleme22eALTN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑁 ≤ ( 𝑂 ∨ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cdleme22.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme22.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme22.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme22.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme22.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme22eALT.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 cdleme22eALT.f ⊢ 𝐹 = ( ( 𝑦 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑦 ) ∧ 𝑊 ) ) )
8 cdleme22eALT.g ⊢ 𝐺 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
9 cdleme22eALT.n ⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) )
10 cdleme22eALT.o ⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
11 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝐾 ∈ HL )
12 11 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝐾 ∈ Lat )
13 simp21l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑃 ∈ 𝐴 )
14 simp22l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑄 ∈ 𝐴 )
15 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16 15 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
17 11 13 14 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
18 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑊 ∈ 𝐻 )
19 simp3ll ⊢ ( ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑦 ∈ 𝐴 )
20 19 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑦 ∈ 𝐴 )
21 1 2 3 4 5 6 7 15 cdleme1b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐹 ∈ ( Base ‘ 𝐾 ) )
22 11 18 13 14 20 21 syl23anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝐹 ∈ ( Base ‘ 𝐾 ) )
23 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑆 ∈ 𝐴 )
24 15 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
25 11 23 20 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑆 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
26 15 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
27 18 26 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
28 15 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
29 12 25 27 28 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
30 15 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
31 12 22 29 30 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
32 15 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
33 12 17 31 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
34 9 33 eqbrtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑁 ≤ ( 𝑃 ∨ 𝑄 ) )
35 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
36 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑇 ∈ 𝐴 )
37 simp321 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑉 ∈ 𝐴 )
38 simp322 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑉 ≤ 𝑊 )
39 37 38 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
40 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑃 ≠ 𝑄 )
41 simp323 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) )
42 1 2 3 4 5 6 cdleme22a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 = 𝑈 )
43 11 18 35 14 36 39 40 41 42 syl233anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑉 = 𝑈 )
44 43 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑂 ∨ 𝑉 ) = ( 𝑂 ∨ 𝑈 ) )
45 10 oveq1i ⊢ ( 𝑂 ∨ 𝑈 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ) ∨ 𝑈 )
46 simp21r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ¬ 𝑃 ≤ 𝑊 )
47 1 2 3 4 5 6 cdleme0a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑈 ∈ 𝐴 )
48 11 18 13 46 14 40 47 syl222anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑈 ∈ 𝐴 )
49 simp3rl ⊢ ( ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑧 ∈ 𝐴 )
50 49 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑧 ∈ 𝐴 )
51 1 2 3 4 5 6 8 15 cdleme1b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → 𝐺 ∈ ( Base ‘ 𝐾 ) )
52 11 18 13 14 50 51 syl23anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝐺 ∈ ( Base ‘ 𝐾 ) )
53 15 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
54 11 36 50 53 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑇 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
55 15 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
56 12 54 27 55 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
57 15 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝐺 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
58 12 52 56 57 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
59 1 2 3 4 5 6 cdlemeulpq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) )
60 11 18 13 14 59 syl22anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) )
61 15 1 2 3 4 atmod2i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) )
62 11 48 17 58 60 61 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) )
63 45 62 eqtr2id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) = ( 𝑂 ∨ 𝑈 ) )
64 43 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑇 ∨ 𝑉 ) = ( 𝑇 ∨ 𝑈 ) )
65 41 64 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑇 ∨ 𝑈 ) )
66 15 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
67 11 36 48 66 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
68 15 4 atbase ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( Base ‘ 𝐾 ) )
69 50 68 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
70 15 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑇 ∨ 𝑈 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ 𝑧 ) )
71 12 67 69 70 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑇 ∨ 𝑈 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ 𝑧 ) )
72 2 4 hlatj32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ 𝑧 ) = ( ( 𝑇 ∨ 𝑧 ) ∨ 𝑈 ) )
73 11 36 48 50 72 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ 𝑧 ) = ( ( 𝑇 ∨ 𝑧 ) ∨ 𝑈 ) )
74 15 4 atbase ⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
75 48 74 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
76 15 2 latj32 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑧 ∨ 𝑈 ) ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑧 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
77 12 69 75 56 76 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑧 ∨ 𝑈 ) ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑧 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
78 15 2 latj32 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐺 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) = ( ( 𝐺 ∨ 𝑈 ) ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
79 12 52 56 75 78 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) = ( ( 𝐺 ∨ 𝑈 ) ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
80 15 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
81 11 13 50 80 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
82 1 2 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑧 ) )
83 11 13 50 82 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑧 ) )
84 15 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑧 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑧 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
85 11 13 81 27 83 84 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑧 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
86 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
87 1 2 86 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
88 11 18 35 87 syl21anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
89 88 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑧 ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑧 ) ∧ ( 1. ‘ 𝐾 ) ) )
90 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
91 11 90 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝐾 ∈ OL )
92 15 3 86 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑧 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑧 ) )
93 91 81 92 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑧 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑧 ) )
94 85 89 93 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑧 ) )
95 94 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑄 ) = ( ( 𝑃 ∨ 𝑧 ) ∨ 𝑄 ) )
96 6 oveq2i ⊢ ( 𝑄 ∨ 𝑈 ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
97 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )
98 11 13 14 97 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )
99 15 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑄 ∨ 𝑊 ) ) )
100 11 14 17 27 98 99 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑄 ∨ 𝑊 ) ) )
101 96 100 syl5eq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑄 ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑄 ∨ 𝑊 ) ) )
102 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
103 1 2 86 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑄 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
104 11 18 102 103 syl21anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑄 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
105 104 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑄 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 1. ‘ 𝐾 ) ) )
106 15 3 86 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑄 ) )
107 91 17 106 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑄 ) )
108 101 105 107 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑄 ∨ 𝑈 ) = ( 𝑃 ∨ 𝑄 ) )
109 108 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑄 ∨ 𝑈 ) ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
110 15 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
111 13 110 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
112 15 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
113 12 81 27 112 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
114 15 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
115 14 114 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
116 15 2 latj32 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑄 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
117 12 111 113 115 116 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑄 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
118 109 117 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑄 ∨ 𝑈 ) ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑄 ) )
119 2 4 hlatj32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) = ( ( 𝑃 ∨ 𝑧 ) ∨ 𝑄 ) )
120 11 13 14 50 119 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) = ( ( 𝑃 ∨ 𝑧 ) ∨ 𝑄 ) )
121 95 118 120 3eqtr4rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) = ( ( 𝑄 ∨ 𝑈 ) ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
122 15 2 latj32 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ∨ 𝑈 ) ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
123 12 115 75 113 122 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑄 ∨ 𝑈 ) ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
124 121 123 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) = ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
125 124 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑧 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) = ( ( 𝑧 ∨ 𝑈 ) ∧ ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) )
126 15 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
127 12 17 69 126 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
128 15 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 𝑧 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) )
129 12 17 69 128 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑧 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) )
130 15 1 2 3 4 atmod1i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) → ( 𝑧 ∨ ( 𝑈 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) ) = ( ( 𝑧 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) )
131 11 50 75 127 129 130 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑧 ∨ ( 𝑈 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) ) = ( ( 𝑧 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) )
132 8 oveq1i ⊢ ( 𝐺 ∨ 𝑈 ) = ( ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ) ∨ 𝑈 )
133 15 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑧 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
134 11 50 48 133 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑧 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
135 15 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
136 12 115 113 135 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
137 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ≤ ( 𝑧 ∨ 𝑈 ) )
138 11 50 48 137 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑈 ≤ ( 𝑧 ∨ 𝑈 ) )
139 15 1 2 3 4 atmod2i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑧 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑈 ≤ ( 𝑧 ∨ 𝑈 ) ) → ( ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ) ∨ 𝑈 ) = ( ( 𝑧 ∨ 𝑈 ) ∧ ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) )
140 11 48 134 136 138 139 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ) ∨ 𝑈 ) = ( ( 𝑧 ∨ 𝑈 ) ∧ ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) )
141 132 140 syl5eq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝐺 ∨ 𝑈 ) = ( ( 𝑧 ∨ 𝑈 ) ∧ ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) )
142 125 131 141 3eqtr4rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝐺 ∨ 𝑈 ) = ( 𝑧 ∨ ( 𝑈 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) ) )
143 15 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) )
144 12 17 69 143 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) )
145 15 1 12 75 17 127 60 144 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) )
146 15 1 3 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ↔ ( 𝑈 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) = 𝑈 ) )
147 12 75 127 146 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑈 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ↔ ( 𝑈 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) = 𝑈 ) )
148 145 147 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑈 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) = 𝑈 )
149 148 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑧 ∨ ( 𝑈 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑧 ) ) ) = ( 𝑧 ∨ 𝑈 ) )
150 142 149 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝐺 ∨ 𝑈 ) = ( 𝑧 ∨ 𝑈 ) )
151 150 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝐺 ∨ 𝑈 ) ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑧 ∨ 𝑈 ) ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
152 79 151 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) = ( ( 𝑧 ∨ 𝑈 ) ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
153 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ≤ ( 𝑇 ∨ 𝑧 ) )
154 11 36 50 153 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑧 ≤ ( 𝑇 ∨ 𝑧 ) )
155 15 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑇 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ≤ ( 𝑇 ∨ 𝑧 ) ) → ( 𝑧 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑇 ∨ 𝑧 ) ∧ ( 𝑧 ∨ 𝑊 ) ) )
156 11 50 54 27 154 155 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑧 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( ( 𝑇 ∨ 𝑧 ) ∧ ( 𝑧 ∨ 𝑊 ) ) )
157 simp33r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) )
158 1 2 86 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) → ( 𝑧 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
159 11 18 157 158 syl21anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑧 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
160 159 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑇 ∨ 𝑧 ) ∧ ( 𝑧 ∨ 𝑊 ) ) = ( ( 𝑇 ∨ 𝑧 ) ∧ ( 1. ‘ 𝐾 ) ) )
161 15 3 86 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑇 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑇 ∨ 𝑧 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑇 ∨ 𝑧 ) )
162 91 54 161 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑇 ∨ 𝑧 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑇 ∨ 𝑧 ) )
163 156 160 162 3eqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑇 ∨ 𝑧 ) = ( 𝑧 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
164 163 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑇 ∨ 𝑧 ) ∨ 𝑈 ) = ( ( 𝑧 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
165 77 152 164 3eqtr4rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑇 ∨ 𝑧 ) ∨ 𝑈 ) = ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
166 73 165 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ 𝑧 ) = ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
167 71 166 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑇 ∨ 𝑈 ) ≤ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
168 65 167 eqbrtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) )
169 15 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
170 12 58 75 169 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
171 15 1 3 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) = ( 𝑃 ∨ 𝑄 ) ) )
172 12 17 170 171 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) = ( 𝑃 ∨ 𝑄 ) ) )
173 168 172 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) ∨ 𝑈 ) ) = ( 𝑃 ∨ 𝑄 ) )
174 44 63 173 3eqtr2rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑂 ∨ 𝑉 ) )
175 34 174 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑁 ≤ ( 𝑂 ∨ 𝑉 ) )