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

Metamath Proof Explorer

Theorem cdleme22cN

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 5th line on p. 115. Show that t \/ v =/= p \/ q and s <_ p \/ q implies -. v <_ p \/ q. (Contributed by NM, 3-Dec-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme22.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme22.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme22.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme22.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme22.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdleme22cN ( ( ( ( 𝐾 ∈ 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 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
7 6 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ Lat )
8 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
9 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
12 6 8 9 11 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
13 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ 𝐻 )
14 10 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
16 10 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
17 7 12 15 16 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
18 simp21r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑆 ≤ 𝑊 )
19 nbrne2 ⊢ ( ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 ∧ ¬ 𝑆 ≤ 𝑊 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≠ 𝑆 )
20 17 18 19 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≠ 𝑆 )
21 simp32l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) )
22 21 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) )
23 6 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ HL )
24 13 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑊 ∈ 𝐻 )
25 simpl12 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
26 simpl13 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ∈ 𝐴 )
27 simp31l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≠ 𝑄 )
28 27 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≠ 𝑄 )
29 simp23l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ∈ 𝐴 )
30 29 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑉 ∈ 𝐴 )
31 simp23r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ≤ 𝑊 )
32 31 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑉 ≤ 𝑊 )
33 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) )
34 eqid ⊢ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
35 1 2 3 4 5 34 cdleme22aa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
36 23 24 25 26 28 30 32 33 35 syl233anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑉 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
37 36 oveq2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑇 ∨ 𝑉 ) = ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
38 22 37 breqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ≤ ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
39 simp32r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
40 39 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
41 simp21l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ 𝐴 )
42 10 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
43 41 42 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
44 simp22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑇 ∈ 𝐴 )
45 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑃 ≤ 𝑊 )
46 1 2 3 4 5 lhpat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐴 )
47 6 13 8 45 9 27 46 syl222anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐴 )
48 10 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐴 ) → ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
49 6 44 47 48 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
50 10 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ 𝑆 ≤ ( ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
51 7 43 49 12 50 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑆 ≤ ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ 𝑆 ≤ ( ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
52 51 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑆 ≤ ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ 𝑆 ≤ ( ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
53 38 40 52 mpbi2and ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ≤ ( ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) )
54 simp31r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ≠ 𝑇 )
55 41 44 54 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) )
56 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) )
57 56 21 39 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) )
58 1 2 3 4 5 cdleme22b ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
59 6 55 8 9 27 29 57 58 syl232anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
60 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
61 6 60 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ AtLat )
62 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
63 10 1 3 62 4 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑇 ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ) )
64 61 44 12 63 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑇 ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ) )
65 59 64 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑇 ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) )
66 65 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑇 ∧ ( 𝑃 ∨ 𝑄 ) ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 0. ‘ 𝐾 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
67 10 4 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
68 44 67 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
69 10 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑄 ) )
70 7 12 15 69 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑄 ) )
71 10 1 2 3 4 atmod4i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐴 ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑇 ∧ ( 𝑃 ∨ 𝑄 ) ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) )
72 6 47 68 12 70 71 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑇 ∧ ( 𝑃 ∨ 𝑄 ) ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) )
73 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
74 6 73 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ OL )
75 10 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
76 7 12 15 75 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
77 10 2 62 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
78 74 76 77 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 0. ‘ 𝐾 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
79 66 72 78 3eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
80 79 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑇 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
81 53 80 breqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
82 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑆 ∈ 𝐴 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐴 ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ↔ 𝑆 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
83 61 41 47 82 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ↔ 𝑆 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
84 83 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ↔ 𝑆 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
85 81 84 mpbid ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
86 85 eqcomd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) = 𝑆 )
87 86 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) = 𝑆 ) )
88 87 necon3ad ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≠ 𝑆 → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) )
89 20 88 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) )