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

Metamath Proof Explorer

Theorem cdleme20j

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114. D , F , Y , G represent s_2, f(s), t_2, f(t). We show s_2 =/= t_2. (Contributed by NM, 18-Nov-2012)

Ref Expression
Hypotheses cdleme19.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme19.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme19.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme19.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme19.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme19.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme19.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
cdleme19.g ⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
cdleme19.d ⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
cdleme19.y ⊢ 𝑌 = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 )
cdleme20.v ⊢ 𝑉 = ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 )
Assertion cdleme20j ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐷 ≠ 𝑌 )

Proof

Step Hyp Ref Expression
1 cdleme19.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme19.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme19.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme19.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme19.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme19.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 cdleme19.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
8 cdleme19.g ⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
9 cdleme19.d ⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
10 cdleme19.y ⊢ 𝑌 = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 )
11 cdleme20.v ⊢ 𝑉 = ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 )
12 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) )
13 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ HL )
14 simp22l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ∈ 𝐴 )
15 simp21l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑅 ∈ 𝐴 )
16 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 16 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
18 13 15 14 17 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
19 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑊 ∈ 𝐻 )
20 16 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21 19 20 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
22 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) )
23 13 15 14 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) )
24 16 1 2 3 4 atmod2i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) ) → ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∨ 𝑆 ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑊 ∨ 𝑆 ) ) )
25 13 14 18 21 23 24 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∨ 𝑆 ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑊 ∨ 𝑆 ) ) )
26 simp22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) )
27 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
28 1 2 27 4 5 lhpjat1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑆 ) = ( 1. ‘ 𝐾 ) )
29 13 19 26 28 syl21anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑊 ∨ 𝑆 ) = ( 1. ‘ 𝐾 ) )
30 29 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑊 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) )
31 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
32 13 31 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ OL )
33 16 3 27 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑅 ∨ 𝑆 ) )
34 32 18 33 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑅 ∨ 𝑆 ) )
35 25 30 34 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∨ 𝑆 ) = ( 𝑅 ∨ 𝑆 ) )
36 35 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∨ 𝑆 ) = ( 𝑅 ∨ 𝑆 ) )
37 simp1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
38 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) )
39 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
40 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) )
41 simp321 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
42 simp322 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
43 41 42 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) )
44 simp323 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
45 1 2 3 4 5 6 7 8 9 10 11 cdleme20d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝐹 ∨ 𝐺 ) ∧ ( 𝐷 ∨ 𝑌 ) ) = 𝑉 )
46 37 26 38 39 40 43 44 45 syl133anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝐹 ∨ 𝐺 ) ∧ ( 𝐷 ∨ 𝑌 ) ) = 𝑉 )
47 13 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ Lat )
48 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑃 ∈ 𝐴 )
49 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑄 ∈ 𝐴 )
50 1 2 3 4 5 6 7 16 cdleme1b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐹 ∈ ( Base ‘ 𝐾 ) )
51 13 19 48 49 14 50 syl23anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐹 ∈ ( Base ‘ 𝐾 ) )
52 simp23l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑇 ∈ 𝐴 )
53 1 2 3 4 5 6 8 16 cdleme1b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐺 ∈ ( Base ‘ 𝐾 ) )
54 13 19 48 49 52 53 syl23anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐺 ∈ ( Base ‘ 𝐾 ) )
55 16 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ ( Base ‘ 𝐾 ) ∧ 𝐺 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ∨ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
56 47 51 54 55 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝐹 ∨ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
57 simp22r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑆 ≤ 𝑊 )
58 1 2 3 4 5 9 cdlemeda ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐷 ∈ 𝐴 )
59 13 19 14 57 15 44 41 58 syl223anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐷 ∈ 𝐴 )
60 simp23r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑇 ≤ 𝑊 )
61 1 2 3 4 5 10 cdlemeda ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑌 ∈ 𝐴 )
62 13 19 52 60 15 44 42 61 syl223anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑌 ∈ 𝐴 )
63 16 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝐷 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐷 ∨ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
64 13 59 62 63 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝐷 ∨ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
65 16 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∨ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐷 ∨ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐹 ∨ 𝐺 ) ∧ ( 𝐷 ∨ 𝑌 ) ) ≤ ( 𝐷 ∨ 𝑌 ) )
66 47 56 64 65 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝐹 ∨ 𝐺 ) ∧ ( 𝐷 ∨ 𝑌 ) ) ≤ ( 𝐷 ∨ 𝑌 ) )
67 46 66 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑉 ≤ ( 𝐷 ∨ 𝑌 ) )
68 67 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑉 ≤ ( 𝐷 ∨ 𝑌 ) )
69 2 4 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝐷 ∈ 𝐴 ) → ( 𝐷 ∨ 𝐷 ) = 𝐷 )
70 13 59 69 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝐷 ∨ 𝐷 ) = 𝐷 )
71 oveq2 ⊢ ( 𝐷 = 𝑌 → ( 𝐷 ∨ 𝐷 ) = ( 𝐷 ∨ 𝑌 ) )
72 70 71 sylan9req ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝐷 = ( 𝐷 ∨ 𝑌 ) )
73 68 72 breqtrrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑉 ≤ 𝐷 )
74 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
75 13 74 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ AtLat )
76 simp31r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ≠ 𝑇 )
77 1 2 3 4 5 11 lhpat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) → 𝑉 ∈ 𝐴 )
78 13 19 14 57 52 76 77 syl222anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑉 ∈ 𝐴 )
79 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑉 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑉 ≤ 𝐷 ↔ 𝑉 = 𝐷 ) )
80 75 78 59 79 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑉 ≤ 𝐷 ↔ 𝑉 = 𝐷 ) )
81 80 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( 𝑉 ≤ 𝐷 ↔ 𝑉 = 𝐷 ) )
82 73 81 mpbid ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑉 = 𝐷 )
83 82 11 eqtr3di ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝐷 = ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) )
84 9 83 eqtr3id ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) = ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) )
85 16 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
86 13 14 52 85 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
87 16 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ ( 𝑆 ∨ 𝑇 ) )
88 47 86 21 87 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ ( 𝑆 ∨ 𝑇 ) )
89 88 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ ( 𝑆 ∨ 𝑇 ) )
90 84 89 eqbrtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑆 ∨ 𝑇 ) )
91 1 2 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) )
92 13 14 52 91 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) )
93 92 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) )
94 16 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
95 47 18 21 94 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
96 16 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
97 14 96 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
98 16 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∨ 𝑆 ) ≤ ( 𝑆 ∨ 𝑇 ) ) )
99 47 95 97 86 98 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∨ 𝑆 ) ≤ ( 𝑆 ∨ 𝑇 ) ) )
100 99 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∨ 𝑆 ) ≤ ( 𝑆 ∨ 𝑇 ) ) )
101 90 93 100 mpbi2and ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∨ 𝑆 ) ≤ ( 𝑆 ∨ 𝑇 ) )
102 36 101 eqbrtrrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( 𝑅 ∨ 𝑆 ) ≤ ( 𝑆 ∨ 𝑇 ) )
103 16 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
104 15 103 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
105 16 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( 𝑆 ∨ 𝑇 ) ) )
106 47 104 97 86 105 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( 𝑆 ∨ 𝑇 ) ) )
107 106 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( 𝑆 ∨ 𝑇 ) ) )
108 102 107 mpbird ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ) )
109 108 simpld ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) )
110 109 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝐷 = 𝑌 → 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) )
111 110 necon3bd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) → 𝐷 ≠ 𝑌 ) )
112 12 111 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐷 ≠ 𝑌 )