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

Metamath Proof Explorer

Theorem cdleme26eALTN

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. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme26.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdleme26.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme26.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme26.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme26.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme26.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme26eALT.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme26eALT.f ⊢ 𝐹 = ( ( 𝑦 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑦 ) ∧ 𝑊 ) ) )
cdleme26eALT.g ⊢ 𝐺 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
cdleme26eALT.n ⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) )
cdleme26eALT.o ⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
cdleme26eALT.i ⊢ 𝐼 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) )
cdleme26eALT.e ⊢ 𝐸 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) )
Assertion cdleme26eALTN ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐼 ≤ ( 𝐸 ∨ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cdleme26.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdleme26.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdleme26.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdleme26.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdleme26.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme26.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme26eALT.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8 cdleme26eALT.f ⊢ 𝐹 = ( ( 𝑦 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑦 ) ∧ 𝑊 ) ) )
9 cdleme26eALT.g ⊢ 𝐺 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
10 cdleme26eALT.n ⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑦 ) ∧ 𝑊 ) ) )
11 cdleme26eALT.o ⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
12 cdleme26eALT.i ⊢ 𝐼 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) )
13 cdleme26eALT.e ⊢ 𝐸 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) )
14 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐾 ∈ HL )
15 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑊 ∈ 𝐻 )
16 simp231 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑇 ∈ 𝐴 )
17 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
18 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
19 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑃 ≠ 𝑄 )
20 simp221 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑆 ∈ 𝐴 )
21 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) )
22 simp21 ⊢ ( ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑦 ∈ 𝐴 )
23 22 3ad2ant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑦 ∈ 𝐴 )
24 simp322 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑦 ≤ 𝑊 )
25 simp31 ⊢ ( ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑧 ∈ 𝐴 )
26 25 3ad2ant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑧 ∈ 𝐴 )
27 simp332 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑧 ≤ 𝑊 )
28 26 27 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) )
29 23 24 28 jca31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) )
30 2 3 4 5 6 7 8 9 10 11 cdleme22eALTN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) ) → 𝑁 ≤ ( 𝑂 ∨ 𝑉 ) )
31 14 15 16 17 18 19 20 21 29 30 syl333anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑁 ≤ ( 𝑂 ∨ 𝑉 ) )
32 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33 simp222 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑆 ≤ 𝑊 )
34 simp223 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
35 1 2 3 4 5 6 7 8 10 12 cdleme25cl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐼 ∈ 𝐵 )
36 32 17 18 20 33 19 34 35 syl322anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐼 ∈ 𝐵 )
37 simp323 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) )
38 1 fvexi ⊢ 𝐵 ∈ V
39 38 12 riotasv ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ∧ ( ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐼 = 𝑁 )
40 36 23 24 37 39 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐼 = 𝑁 )
41 simp232 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑇 ≤ 𝑊 )
42 simp233 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
43 1 2 3 4 5 6 7 9 11 13 cdleme25cl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐸 ∈ 𝐵 )
44 32 17 18 16 41 19 42 43 syl322anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐸 ∈ 𝐵 )
45 simp333 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) )
46 38 13 riotasv ⊢ ( ( 𝐸 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐸 = 𝑂 )
47 44 26 27 45 46 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐸 = 𝑂 )
48 47 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝐸 ∨ 𝑉 ) = ( 𝑂 ∨ 𝑉 ) )
49 31 40 48 3brtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑊 ∧ ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐼 ≤ ( 𝐸 ∨ 𝑉 ) )