Metamath Proof Explorer

Theorem cdleme26e

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, 2-Feb-2013)

Ref Expression
Hypotheses cdleme26.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdleme26.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme26.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme26.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme26.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme26.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme26e.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme26e.f ⊢ 𝐹 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
cdleme26e.n ⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑧 ) ∧ 𝑊 ) ) )
cdleme26e.o ⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
cdleme26e.i ⊢ 𝐼 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) )
cdleme26e.e ⊢ 𝐸 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) )
Assertion cdleme26e ( ( ( ( 𝐾 ∈ 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 cdleme26e.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8 cdleme26e.f ⊢ 𝐹 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
9 cdleme26e.n ⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑆 ∨ 𝑧 ) ∧ 𝑊 ) ) )
10 cdleme26e.o ⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) ) )
11 cdleme26e.i ⊢ 𝐼 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) )
12 cdleme26e.e ⊢ 𝐸 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) )
13 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
15 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
16 simp21l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑆 ∈ 𝐴 )
17 simp22l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑇 ∈ 𝐴 )
18 16 17 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) )
19 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
20 simp311 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑃 ≠ 𝑄 )
21 simp32l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) )
22 20 21 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) )
23 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) )
24 2 3 4 5 6 7 8 9 10 cdleme22e ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑁 ≤ ( 𝑂 ∨ 𝑉 ) )
25 13 14 15 18 19 22 23 24 syl133anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑁 ≤ ( 𝑂 ∨ 𝑉 ) )
26 simp21r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ¬ 𝑆 ≤ 𝑊 )
27 simp312 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
28 1 2 3 4 5 6 7 8 9 11 cdleme25cl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐼 ∈ 𝐵 )
29 13 14 15 16 26 20 27 28 syl322anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝐼 ∈ 𝐵 )
30 simp33l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑧 ∈ 𝐴 )
31 simp33r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ¬ 𝑧 ≤ 𝑊 )
32 simp32r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) )
33 31 32 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) )
34 1 fvexi ⊢ 𝐵 ∈ V
35 34 11 riotasv ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐼 = 𝑁 )
36 29 30 33 35 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝐼 = 𝑁 )
37 simp22r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ¬ 𝑇 ≤ 𝑊 )
38 simp313 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
39 1 2 3 4 5 6 7 8 10 12 cdleme25cl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐸 ∈ 𝐵 )
40 13 14 15 17 37 20 38 39 syl322anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝐸 ∈ 𝐵 )
41 34 12 riotasv ⊢ ( ( 𝐸 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐸 = 𝑂 )
42 40 30 33 41 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝐸 = 𝑂 )
43 42 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → ( 𝐸 ∨ 𝑉 ) = ( 𝑂 ∨ 𝑉 ) )
44 25 36 43 3brtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ) → 𝐼 ≤ ( 𝐸 ∨ 𝑉 ) )