Theorem cdleme27a 37497

Description: Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 37493 with s and t swapped (this case is not mentioned by them). If s ≤ t ∨ v, then f(s) ≤ f_s(t) ∨ v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.)

Hypotheses

Ref	Expression
cdleme26.b	⊢ 𝐵 = (Base‘𝐾)
cdleme26.l	⊢ ≤ = (le‘𝐾)
cdleme26.j	⊢ ∨ = (join‘𝐾)
cdleme26.m	⊢ ∧ = (meet‘𝐾)
cdleme26.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme26.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme27.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdleme27.f	⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
cdleme27.z	⊢ 𝑍 = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
cdleme27.n	⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝑍 ∨ ((𝑠 ∨ 𝑧) ∧ 𝑊)))
cdleme27.d	⊢ 𝐷 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁))
cdleme27.c	⊢ 𝐶 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐷, 𝐹)
cdleme27.g	⊢ 𝐺 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
cdleme27.o	⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝑍 ∨ ((𝑡 ∨ 𝑧) ∧ 𝑊)))
cdleme27.e	⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
cdleme27.y	⊢ 𝑌 = if(𝑡 ≤ (𝑃 ∨ 𝑄), 𝐸, 𝐺)

Assertion

Ref	Expression
cdleme27a	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉))

Distinct variable groups:   𝑡,𝑠,𝑢,𝑧,𝐴   𝐵,𝑠,𝑡,𝑢,𝑧   𝑢,𝐹   𝑢,𝐺   𝐻,𝑠,𝑡,𝑧   ∨ ,𝑠,𝑡,𝑢,𝑧   𝐾,𝑠,𝑡,𝑧   ≤ ,𝑠,𝑡,𝑢,𝑧   ∧ ,𝑠,𝑡,𝑢,𝑧   𝑡,𝑁,𝑢   𝑂,𝑠,𝑢   𝑃,𝑠,𝑡,𝑢,𝑧   𝑄,𝑠,𝑡,𝑢,𝑧   𝑈,𝑠,𝑡,𝑢,𝑧   𝑧,𝑉   𝑊,𝑠,𝑡,𝑢,𝑧

Allowed substitution hints:   𝐶(𝑧,𝑢,𝑡,𝑠)   𝐷(𝑧,𝑢,𝑡,𝑠)   𝐸(𝑧,𝑢,𝑡,𝑠)   𝐹(𝑧,𝑡,𝑠)   𝐺(𝑧,𝑡,𝑠)   𝐻(𝑢)   𝐾(𝑢)   𝑁(𝑧,𝑠)   𝑂(𝑧,𝑡)   𝑉(𝑢,𝑡,𝑠)   𝑌(𝑧,𝑢,𝑡,𝑠)   𝑍(𝑧,𝑢,𝑡,𝑠)

Proof of Theorem cdleme27a

Step	Hyp	Ref	Expression
1		simp211 1307	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp221 1310	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
3		simp222 1311	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
4		simp213 1309	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊))
5		simp223 1312	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
6		simp23r 1291	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
7		simp212 1308	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑄)
8		simp1l 1193	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → 𝑠 ≤ (𝑃 ∨ 𝑄))
9		simp1r 1194	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → 𝑡 ≤ (𝑃 ∨ 𝑄))
10	7, 8, 9	3jca 1124	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑃 ≠ 𝑄 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)))
11		simp3 1134	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄))
12		cdleme26.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐾)
13		cdleme26.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
14		cdleme26.j	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
15		cdleme26.m	. . . . . . . 8 ⊢ ∧ = (meet‘𝐾)
16		cdleme26.a	. . . . . . . 8 ⊢ 𝐴 = (Atoms‘𝐾)
17		cdleme26.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
18		cdleme27.u	. . . . . . . 8 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
19		cdleme27.z	. . . . . . . 8 ⊢ 𝑍 = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
20		cdleme27.n	. . . . . . . 8 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝑍 ∨ ((𝑠 ∨ 𝑧) ∧ 𝑊)))
21		cdleme27.o	. . . . . . . 8 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝑍 ∨ ((𝑡 ∨ 𝑧) ∧ 𝑊)))
22		cdleme27.d	. . . . . . . 8 ⊢ 𝐷 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁))
23		cdleme27.e	. . . . . . . 8 ⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
24	12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23	cdleme26ee 37490	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄))) → 𝐷 ≤ (𝐸 ∨ 𝑉))
25	1, 2, 3, 4, 5, 6, 10, 11, 24	syl332anc 1397	. . . . . 6 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → 𝐷 ≤ (𝐸 ∨ 𝑉))
26	25	3expia 1117	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ((𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄) → 𝐷 ≤ (𝐸 ∨ 𝑉)))
27		simp1r 1194	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑡 ≤ (𝑃 ∨ 𝑄))
28		simp11l 1280	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐾 ∈ HL)
29	28	3ad2ant2 1130	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝐾 ∈ HL)
30		simp13l 1284	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑠 ∈ 𝐴)
31	30	3ad2ant2 1130	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑠 ∈ 𝐴)
32		simp23l 1290	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑡 ∈ 𝐴)
33	32	3ad2ant2 1130	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑡 ∈ 𝐴)
34		simp3ll 1240	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑠 ≠ 𝑡)
35	34	3ad2ant2 1130	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑠 ≠ 𝑡)
36	31, 33, 35	3jca 1124	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → (𝑠 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ∧ 𝑠 ≠ 𝑡))
37		simp21l 1286	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑃 ∈ 𝐴)
38	37	3ad2ant2 1130	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑃 ∈ 𝐴)
39		simp22l 1288	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑄 ∈ 𝐴)
40	39	3ad2ant2 1130	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑄 ∈ 𝐴)
41		simp212 1308	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑄)
42		simp3rl 1242	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑉 ∈ 𝐴)
43	42	3ad2ant2 1130	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑉 ∈ 𝐴)
44		simp3 1134	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄))
45		simp3lr 1241	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑠 ≤ (𝑡 ∨ 𝑉))
46	45	3ad2ant2 1130	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑠 ≤ (𝑡 ∨ 𝑉))
47		simp1l 1193	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑠 ≤ (𝑃 ∨ 𝑄))
48	44, 46, 47	3jca 1124	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → ((𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄) ∧ 𝑠 ≤ (𝑡 ∨ 𝑉) ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)))
49	13, 14, 15, 16, 17	cdleme22b 37471	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑠 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ∧ 𝑠 ≠ 𝑡)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑉 ∈ 𝐴 ∧ ((𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄) ∧ 𝑠 ≤ (𝑡 ∨ 𝑉) ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)))) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
50	29, 36, 38, 40, 41, 43, 48, 49	syl232anc 1393	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
51	27, 50	pm2.21dd 197	. . . . . 6 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝐷 ≤ (𝐸 ∨ 𝑉))
52	51	3expia 1117	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ((𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄) → 𝐷 ≤ (𝐸 ∨ 𝑉)))
53	26, 52	pm2.61dne 3103	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐷 ≤ (𝐸 ∨ 𝑉))
54		cdleme27.c	. . . . . 6 ⊢ 𝐶 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐷, 𝐹)
55		iftrue 4472	. . . . . 6 ⊢ (𝑠 ≤ (𝑃 ∨ 𝑄) → if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐷, 𝐹) = 𝐷)
56	54, 55	syl5eq 2868	. . . . 5 ⊢ (𝑠 ≤ (𝑃 ∨ 𝑄) → 𝐶 = 𝐷)
57	56	ad2antrr 724	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 = 𝐷)
58		cdleme27.y	. . . . . . 7 ⊢ 𝑌 = if(𝑡 ≤ (𝑃 ∨ 𝑄), 𝐸, 𝐺)
59		iftrue 4472	. . . . . . 7 ⊢ (𝑡 ≤ (𝑃 ∨ 𝑄) → if(𝑡 ≤ (𝑃 ∨ 𝑄), 𝐸, 𝐺) = 𝐸)
60	58, 59	syl5eq 2868	. . . . . 6 ⊢ (𝑡 ≤ (𝑃 ∨ 𝑄) → 𝑌 = 𝐸)
61	60	oveq1d 7165	. . . . 5 ⊢ (𝑡 ≤ (𝑃 ∨ 𝑄) → (𝑌 ∨ 𝑉) = (𝐸 ∨ 𝑉))
62	61	ad2antlr 725	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑌 ∨ 𝑉) = (𝐸 ∨ 𝑉))
63	53, 57, 62	3brtr4d 5090	. . 3 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 ≤ (𝑌 ∨ 𝑉))
64	63	ex 415	. 2 ⊢ ((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉)))
65		simpr11 1253	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
66		simpr12 1254	. . . . . 6 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑃 ≠ 𝑄)
67		simpll 765	. . . . . 6 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑠 ≤ (𝑃 ∨ 𝑄))
68	66, 67	jca 514	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ≠ 𝑄 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)))
69		simpr23 1258	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
70		simpr21 1256	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
71		simpr22 1257	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
72		simpr13 1255	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊))
73		simplr 767	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
74		simpr3l 1230	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)))
75		simpr3r 1231	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
76		cdleme27.g	. . . . . 6 ⊢ 𝐺 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
77		eqid 2821	. . . . . 6 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
78		eqid 2821	. . . . . . 7 ⊢ (℩𝑢 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))))) = (℩𝑢 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))))
79	19, 20, 76, 77, 22, 78	cdleme25cv 37488	. . . . . 6 ⊢ 𝐷 = (℩𝑢 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))))
80	12, 13, 14, 15, 16, 17, 18, 76, 77, 79	cdleme26f 37493	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ≠ 𝑄 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) ∧ (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐷 ≤ (𝐺 ∨ 𝑉))
81	65, 68, 69, 70, 71, 72, 73, 74, 75, 80	syl333anc 1398	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐷 ≤ (𝐺 ∨ 𝑉))
82	56	ad2antrr 724	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 = 𝐷)
83		iffalse 4475	. . . . . . 7 ⊢ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) → if(𝑡 ≤ (𝑃 ∨ 𝑄), 𝐸, 𝐺) = 𝐺)
84	58, 83	syl5eq 2868	. . . . . 6 ⊢ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) → 𝑌 = 𝐺)
85	84	oveq1d 7165	. . . . 5 ⊢ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) → (𝑌 ∨ 𝑉) = (𝐺 ∨ 𝑉))
86	85	ad2antlr 725	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑌 ∨ 𝑉) = (𝐺 ∨ 𝑉))
87	81, 82, 86	3brtr4d 5090	. . 3 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 ≤ (𝑌 ∨ 𝑉))
88	87	ex 415	. 2 ⊢ ((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉)))
89		simpr11 1253	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
90		simpr12 1254	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑃 ≠ 𝑄)
91		simplr 767	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑡 ≤ (𝑃 ∨ 𝑄))
92	90, 91	jca 514	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ≠ 𝑄 ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)))
93		simpr13 1255	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊))
94		simpr21 1256	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
95		simpr22 1257	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
96		simpr23 1258	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
97		simpll 765	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ¬ 𝑠 ≤ (𝑃 ∨ 𝑄))
98		simpr3l 1230	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)))
99		simpr3r 1231	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
100		cdleme27.f	. . . . . 6 ⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
101		eqid 2821	. . . . . 6 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊)))
102		eqid 2821	. . . . . . 7 ⊢ (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊))))) = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊)))))
103	19, 21, 100, 101, 23, 102	cdleme25cv 37488	. . . . . 6 ⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊)))))
104	12, 13, 14, 15, 16, 17, 18, 100, 101, 103	cdleme26f2 37495	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ≠ 𝑄 ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐹 ≤ (𝐸 ∨ 𝑉))
105	89, 92, 93, 94, 95, 96, 97, 98, 99, 104	syl333anc 1398	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐹 ≤ (𝐸 ∨ 𝑉))
106		iffalse 4475	. . . . . 6 ⊢ (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) → if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐷, 𝐹) = 𝐹)
107	54, 106	syl5eq 2868	. . . . 5 ⊢ (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) → 𝐶 = 𝐹)
108	107	ad2antrr 724	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 = 𝐹)
109	61	ad2antlr 725	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑌 ∨ 𝑉) = (𝐸 ∨ 𝑉))
110	105, 108, 109	3brtr4d 5090	. . 3 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 ≤ (𝑌 ∨ 𝑉))
111	110	ex 415	. 2 ⊢ ((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉)))
112		simpr11 1253	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
113		simpr23 1258	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
114		simplr 767	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
115		simpll 765	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ¬ 𝑠 ≤ (𝑃 ∨ 𝑄))
116		simpr12 1254	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑃 ≠ 𝑄)
117	114, 115, 116	3jca 1124	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄))
118		simpr21 1256	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
119		simpr22 1257	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
120		simpr13 1255	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊))
121		simpr3l 1230	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)))
122		simpr3r 1231	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
123	13, 14, 15, 16, 17, 18, 100, 76	cdleme22g 37478	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐹 ≤ (𝐺 ∨ 𝑉))
124	112, 113, 117, 118, 119, 120, 121, 122, 123	syl323anc 1396	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐹 ≤ (𝐺 ∨ 𝑉))
125	107	ad2antrr 724	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 = 𝐹)
126	85	ad2antlr 725	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑌 ∨ 𝑉) = (𝐺 ∨ 𝑉))
127	124, 125, 126	3brtr4d 5090	. . 3 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 ≤ (𝑌 ∨ 𝑉))
128	127	ex 415	. 2 ⊢ ((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉)))
129	64, 88, 111, 128	4cases 1035	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ifcif 4466   class class class wbr 5058  ‘cfv 6349  ℩crio 7107  (class class class)co 7150  Basecbs 16477  lecple 16566  joincjn 17548  meetcmee 17549  Atomscatm 36393  HLchlt 36480  LHypclh 37114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-riotaBAD 36083

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-iin 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-undef 7933  df-proset 17532  df-poset 17550  df-plt 17562  df-lub 17578  df-glb 17579  df-join 17580  df-meet 17581  df-p0 17643  df-p1 17644  df-lat 17650  df-clat 17712  df-oposet 36306  df-ol 36308  df-oml 36309  df-covers 36396  df-ats 36397  df-atl 36428  df-cvlat 36452  df-hlat 36481  df-llines 36628  df-lplanes 36629  df-lvols 36630  df-lines 36631  df-psubsp 36633  df-pmap 36634  df-padd 36926  df-lhyp 37118

This theorem is referenced by:  cdleme27N  37499  cdleme28a  37500