Metamath Proof Explorer

Theorem cdleme22e

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)

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