Theorem cdleme27a 36981

Description: Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 36977 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 1292	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp221 1295	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
3		simp222 1296	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
4		simp213 1294	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊))
5		simp223 1297	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
6		simp23r 1276	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
7		simp212 1293	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑄)
8		simp1l 1178	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → 𝑠 ≤ (𝑃 ∨ 𝑄))
9		simp1r 1179	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → 𝑡 ≤ (𝑃 ∨ 𝑄))
10	7, 8, 9	3jca 1109	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → (𝑃 ≠ 𝑄 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)))
11		simp3 1119	. . . . . . 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 36974	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄))) → 𝐷 ≤ (𝐸 ∨ 𝑉))
25	1, 2, 3, 4, 5, 6, 10, 11, 24	syl332anc 1382	. . . . . 6 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄)) → 𝐷 ≤ (𝐸 ∨ 𝑉))
26	25	3expia 1102	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ((𝑡 ∨ 𝑉) = (𝑃 ∨ 𝑄) → 𝐷 ≤ (𝐸 ∨ 𝑉)))
27		simp1r 1179	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑡 ≤ (𝑃 ∨ 𝑄))
28		simp11l 1265	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐾 ∈ HL)
29	28	3ad2ant2 1115	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝐾 ∈ HL)
30		simp13l 1269	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑠 ∈ 𝐴)
31	30	3ad2ant2 1115	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑠 ∈ 𝐴)
32		simp23l 1275	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑡 ∈ 𝐴)
33	32	3ad2ant2 1115	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑡 ∈ 𝐴)
34		simp3ll 1225	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑠 ≠ 𝑡)
35	34	3ad2ant2 1115	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑠 ≠ 𝑡)
36	31, 33, 35	3jca 1109	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → (𝑠 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ∧ 𝑠 ≠ 𝑡))
37		simp21l 1271	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑃 ∈ 𝐴)
38	37	3ad2ant2 1115	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑃 ∈ 𝐴)
39		simp22l 1273	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑄 ∈ 𝐴)
40	39	3ad2ant2 1115	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑄 ∈ 𝐴)
41		simp212 1293	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑄)
42		simp3rl 1227	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑉 ∈ 𝐴)
43	42	3ad2ant2 1115	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑉 ∈ 𝐴)
44		simp3 1119	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄))
45		simp3lr 1226	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝑠 ≤ (𝑡 ∨ 𝑉))
46	45	3ad2ant2 1115	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑠 ≤ (𝑡 ∨ 𝑉))
47		simp1l 1178	. . . . . . . . 9 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝑠 ≤ (𝑃 ∨ 𝑄))
48	44, 46, 47	3jca 1109	. . . . . . . 8 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → ((𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄) ∧ 𝑠 ≤ (𝑡 ∨ 𝑉) ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)))
49	13, 14, 15, 16, 17	cdleme22b 36955	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑠 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ∧ 𝑠 ≠ 𝑡)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑉 ∈ 𝐴 ∧ ((𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄) ∧ 𝑠 ≤ (𝑡 ∨ 𝑉) ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)))) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
50	29, 36, 38, 40, 41, 43, 48, 49	syl232anc 1378	. . . . . . 7 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
51	27, 50	pm2.21dd 187	. . . . . 6 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) ∧ (𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄)) → 𝐷 ≤ (𝐸 ∨ 𝑉))
52	51	3expia 1102	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ((𝑡 ∨ 𝑉) ≠ (𝑃 ∨ 𝑄) → 𝐷 ≤ (𝐸 ∨ 𝑉)))
53	26, 52	pm2.61dne 3049	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐷 ≤ (𝐸 ∨ 𝑉))
54		cdleme27.c	. . . . . 6 ⊢ 𝐶 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐷, 𝐹)
55		iftrue 4351	. . . . . 6 ⊢ (𝑠 ≤ (𝑃 ∨ 𝑄) → if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐷, 𝐹) = 𝐷)
56	54, 55	syl5eq 2821	. . . . 5 ⊢ (𝑠 ≤ (𝑃 ∨ 𝑄) → 𝐶 = 𝐷)
57	56	ad2antrr 714	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 = 𝐷)
58		cdleme27.y	. . . . . . 7 ⊢ 𝑌 = if(𝑡 ≤ (𝑃 ∨ 𝑄), 𝐸, 𝐺)
59		iftrue 4351	. . . . . . 7 ⊢ (𝑡 ≤ (𝑃 ∨ 𝑄) → if(𝑡 ≤ (𝑃 ∨ 𝑄), 𝐸, 𝐺) = 𝐸)
60	58, 59	syl5eq 2821	. . . . . 6 ⊢ (𝑡 ≤ (𝑃 ∨ 𝑄) → 𝑌 = 𝐸)
61	60	oveq1d 6990	. . . . 5 ⊢ (𝑡 ≤ (𝑃 ∨ 𝑄) → (𝑌 ∨ 𝑉) = (𝐸 ∨ 𝑉))
62	61	ad2antlr 715	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑌 ∨ 𝑉) = (𝐸 ∨ 𝑉))
63	53, 57, 62	3brtr4d 4958	. . 3 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 ≤ (𝑌 ∨ 𝑉))
64	63	ex 405	. 2 ⊢ ((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉)))
65		simpr11 1238	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
66		simpr12 1239	. . . . . 6 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑃 ≠ 𝑄)
67		simpll 755	. . . . . 6 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑠 ≤ (𝑃 ∨ 𝑄))
68	66, 67	jca 504	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ≠ 𝑄 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)))
69		simpr23 1243	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
70		simpr21 1241	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
71		simpr22 1242	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
72		simpr13 1240	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊))
73		simplr 757	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
74		simpr3l 1215	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)))
75		simpr3r 1216	. . . . 5 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
76		cdleme27.g	. . . . . 6 ⊢ 𝐺 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
77		eqid 2773	. . . . . 6 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
78		eqid 2773	. . . . . . 7 ⊢ (℩𝑢 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))))) = (℩𝑢 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))))
79	19, 20, 76, 77, 22, 78	cdleme25cv 36972	. . . . . 6 ⊢ 𝐷 = (℩𝑢 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))))
80	12, 13, 14, 15, 16, 17, 18, 76, 77, 79	cdleme26f 36977	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ≠ 𝑄 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) ∧ (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐷 ≤ (𝐺 ∨ 𝑉))
81	65, 68, 69, 70, 71, 72, 73, 74, 75, 80	syl333anc 1383	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐷 ≤ (𝐺 ∨ 𝑉))
82	56	ad2antrr 714	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 = 𝐷)
83		iffalse 4354	. . . . . . 7 ⊢ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) → if(𝑡 ≤ (𝑃 ∨ 𝑄), 𝐸, 𝐺) = 𝐺)
84	58, 83	syl5eq 2821	. . . . . 6 ⊢ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) → 𝑌 = 𝐺)
85	84	oveq1d 6990	. . . . 5 ⊢ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) → (𝑌 ∨ 𝑉) = (𝐺 ∨ 𝑉))
86	85	ad2antlr 715	. . . 4 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑌 ∨ 𝑉) = (𝐺 ∨ 𝑉))
87	81, 82, 86	3brtr4d 4958	. . 3 ⊢ (((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 ≤ (𝑌 ∨ 𝑉))
88	87	ex 405	. 2 ⊢ ((𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉)))
89		simpr11 1238	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
90		simpr12 1239	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑃 ≠ 𝑄)
91		simplr 757	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑡 ≤ (𝑃 ∨ 𝑄))
92	90, 91	jca 504	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ≠ 𝑄 ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)))
93		simpr13 1240	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊))
94		simpr21 1241	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
95		simpr22 1242	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
96		simpr23 1243	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
97		simpll 755	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ¬ 𝑠 ≤ (𝑃 ∨ 𝑄))
98		simpr3l 1215	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)))
99		simpr3r 1216	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
100		cdleme27.f	. . . . . 6 ⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
101		eqid 2773	. . . . . 6 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊)))
102		eqid 2773	. . . . . . 7 ⊢ (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊))))) = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊)))))
103	19, 21, 100, 101, 23, 102	cdleme25cv 36972	. . . . . 6 ⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑡 ∨ 𝑠) ∧ 𝑊)))))
104	12, 13, 14, 15, 16, 17, 18, 100, 101, 103	cdleme26f2 36979	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ≠ 𝑄 ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐹 ≤ (𝐸 ∨ 𝑉))
105	89, 92, 93, 94, 95, 96, 97, 98, 99, 104	syl333anc 1383	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐹 ≤ (𝐸 ∨ 𝑉))
106		iffalse 4354	. . . . . 6 ⊢ (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) → if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐷, 𝐹) = 𝐹)
107	54, 106	syl5eq 2821	. . . . 5 ⊢ (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) → 𝐶 = 𝐹)
108	107	ad2antrr 714	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 = 𝐹)
109	61	ad2antlr 715	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑌 ∨ 𝑉) = (𝐸 ∨ 𝑉))
110	105, 108, 109	3brtr4d 4958	. . 3 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 ≤ (𝑌 ∨ 𝑉))
111	110	ex 405	. 2 ⊢ ((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑡 ≤ (𝑃 ∨ 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉)))
112		simpr11 1238	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
113		simpr23 1243	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
114		simplr 757	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
115		simpll 755	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → ¬ 𝑠 ≤ (𝑃 ∨ 𝑄))
116		simpr12 1239	. . . . . 6 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝑃 ≠ 𝑄)
117	114, 115, 116	3jca 1109	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄))
118		simpr21 1241	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
119		simpr22 1242	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
120		simpr13 1240	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊))
121		simpr3l 1215	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)))
122		simpr3r 1216	. . . . 5 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
123	13, 14, 15, 16, 17, 18, 100, 76	cdleme22g 36962	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ (𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐹 ≤ (𝐺 ∨ 𝑉))
124	112, 113, 117, 118, 119, 120, 121, 122, 123	syl323anc 1381	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐹 ≤ (𝐺 ∨ 𝑉))
125	107	ad2antrr 714	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 = 𝐹)
126	85	ad2antlr 715	. . . 4 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → (𝑌 ∨ 𝑉) = (𝐺 ∨ 𝑉))
127	124, 125, 126	3brtr4d 4958	. . 3 ⊢ (((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)))) → 𝐶 ≤ (𝑌 ∨ 𝑉))
128	127	ex 405	. 2 ⊢ ((¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉)))
129	64, 88, 111, 128	4cases 1022	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ ((𝑠 ≠ 𝑡 ∧ 𝑠 ≤ (𝑡 ∨ 𝑉)) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))) → 𝐶 ≤ (𝑌 ∨ 𝑉))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 387   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051   ≠ wne 2962  ∀wral 3083  ifcif 4345   class class class wbr 4926  ‘cfv 6186  ℩crio 6935  (class class class)co 6975  Basecbs 16338  lecple 16427  joincjn 17425  meetcmee 17426  Atomscatm 35877  HLchlt 35964  LHypclh 36598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-riotaBAD 35567

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-iun 4791  df-iin 4792  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-1st 7500  df-2nd 7501  df-undef 7741  df-proset 17409  df-poset 17427  df-plt 17439  df-lub 17455  df-glb 17456  df-join 17457  df-meet 17458  df-p0 17520  df-p1 17521  df-lat 17527  df-clat 17589  df-oposet 35790  df-ol 35792  df-oml 35793  df-covers 35880  df-ats 35881  df-atl 35912  df-cvlat 35936  df-hlat 35965  df-llines 36112  df-lplanes 36113  df-lvols 36114  df-lines 36115  df-psubsp 36117  df-pmap 36118  df-padd 36410  df-lhyp 36602

This theorem is referenced by:  cdleme27N  36983  cdleme28a  36984