cdleme20l2 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdleme20l2		Structured version Visualization version GIF version

Theorem cdleme20l2 38262

Description: Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. 𝐷, 𝐹, 𝑌, 𝐺 represent s₂, f(s), t₂, f(t) respectively. (Contributed by NM, 20-Nov-2012.)

**Hypotheses**
Ref	Expression
cdleme19.l	⊢ ≤ = (le‘𝐾)
cdleme19.j	⊢ ∨ = (join‘𝐾)
cdleme19.m	⊢ ∧ = (meet‘𝐾)
cdleme19.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme19.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme19.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdleme19.f	⊢ 𝐹 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
cdleme19.g	⊢ 𝐺 = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑇) ∧ 𝑊)))
cdleme19.d	⊢ 𝐷 = ((𝑅 ∨ 𝑆) ∧ 𝑊)
cdleme19.y	⊢ 𝑌 = ((𝑅 ∨ 𝑇) ∧ 𝑊)
cdleme20.v	⊢ 𝑉 = ((𝑆 ∨ 𝑇) ∧ 𝑊)

**Assertion**
Ref	Expression
cdleme20l2	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ 𝑌)) ∈ 𝐴)

**Proof of Theorem cdleme20l2**
Step	Hyp	Ref	Expression
1		simp11l 1282	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐾 ∈ HL)
2	1	hllatd 37305	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐾 ∈ Lat)
3		simp11r 1283	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑊 ∈ 𝐻)
4		simp12l 1284	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑃 ∈ 𝐴)
5		simp13l 1286	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑄 ∈ 𝐴)
6		simp22l 1290	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑆 ∈ 𝐴)
7		cdleme19.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
8		cdleme19.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
9		cdleme19.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
10		cdleme19.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
11		cdleme19.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
12		cdleme19.u	. . . . . 6 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
13		cdleme19.f	. . . . . 6 ⊢ 𝐹 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
14		eqid 2738	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
15	7, 8, 9, 10, 11, 12, 13, 14	cdleme1b 38167	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝐹 ∈ (Base‘𝐾))
16	1, 3, 4, 5, 6, 15	syl23anc 1375	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐹 ∈ (Base‘𝐾))
17		simp21l 1288	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑅 ∈ 𝐴)
18		cdleme19.d	. . . . . 6 ⊢ 𝐷 = ((𝑅 ∨ 𝑆) ∧ 𝑊)
19	7, 8, 9, 10, 11, 18, 14	cdlemedb 38238	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝐷 ∈ (Base‘𝐾))
20	1, 3, 17, 6, 19	syl22anc 835	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐷 ∈ (Base‘𝐾))
21		simp23l 1292	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑇 ∈ 𝐴)
22		cdleme19.g	. . . . . 6 ⊢ 𝐺 = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑇) ∧ 𝑊)))
23	7, 8, 9, 10, 11, 12, 22, 14	cdleme1b 38167	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) → 𝐺 ∈ (Base‘𝐾))
24	1, 3, 4, 5, 21, 23	syl23anc 1375	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐺 ∈ (Base‘𝐾))
25		cdleme19.y	. . . . . 6 ⊢ 𝑌 = ((𝑅 ∨ 𝑇) ∧ 𝑊)
26	7, 8, 9, 10, 11, 25, 14	cdlemedb 38238	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) → 𝑌 ∈ (Base‘𝐾))
27	1, 3, 17, 21, 26	syl22anc 835	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑌 ∈ (Base‘𝐾))
28	14, 8	latj4 18122	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ (Base‘𝐾) ∧ 𝐷 ∈ (Base‘𝐾)) ∧ (𝐺 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾))) → ((𝐹 ∨ 𝐷) ∨ (𝐺 ∨ 𝑌)) = ((𝐹 ∨ 𝐺) ∨ (𝐷 ∨ 𝑌)))
29	2, 16, 20, 24, 27, 28	syl122anc 1377	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ((𝐹 ∨ 𝐷) ∨ (𝐺 ∨ 𝑌)) = ((𝐹 ∨ 𝐺) ∨ (𝐷 ∨ 𝑌)))
30		simp1 1134	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
31		simp22 1205	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))
32		simp23 1206	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊))
33		simp21 1204	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))
34		simp31 1207	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇))
35		simp321 1321	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))
36		simp322 1322	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑇 ≤ (𝑃 ∨ 𝑄))
37	35, 36	jca 511	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)))
38		simp323 1323	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
39		cdleme20.v	. . . . . . 7 ⊢ 𝑉 = ((𝑆 ∨ 𝑇) ∧ 𝑊)
40	7, 8, 9, 10, 11, 12, 13, 22, 18, 25, 39	cdleme20d 38253	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝐹 ∨ 𝐺) ∧ (𝐷 ∨ 𝑌)) = 𝑉)
41	30, 31, 32, 33, 34, 37, 38, 40	syl133anc 1391	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ((𝐹 ∨ 𝐺) ∧ (𝐷 ∨ 𝑌)) = 𝑉)
42		simp22r 1291	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑆 ≤ 𝑊)
43		simp31r 1295	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑆 ≠ 𝑇)
44	7, 8, 9, 10, 11, 39	lhpat2 37986	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) → 𝑉 ∈ 𝐴)
45	1, 3, 6, 42, 21, 43, 44	syl222anc 1384	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑉 ∈ 𝐴)
46	41, 45	eqeltrd 2839	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ((𝐹 ∨ 𝐺) ∧ (𝐷 ∨ 𝑌)) ∈ 𝐴)
47		simp11 1201	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
48		simp12 1202	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
49		simp13 1203	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
50		simp31l 1294	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑃 ≠ 𝑄)
51	7, 8, 9, 10, 11, 12, 13	cdleme3fa 38177	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → 𝐹 ∈ 𝐴)
52	47, 48, 49, 31, 50, 35, 51	syl132anc 1386	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐹 ∈ 𝐴)
53	7, 8, 9, 10, 11, 12, 22	cdleme3fa 38177	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄))) → 𝐺 ∈ 𝐴)
54	47, 48, 49, 32, 50, 36, 53	syl132anc 1386	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐺 ∈ 𝐴)
55		simp33r 1299	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))
56	7, 8, 9, 10, 11, 12, 13, 22	cdleme16b 38220	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝐹 ≠ 𝐺)
57	30, 31, 32, 34, 35, 36, 55, 56	syl133anc 1391	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐹 ≠ 𝐺)
58		eqid 2738	. . . . . . 7 ⊢ (LLines‘𝐾) = (LLines‘𝐾)
59	8, 10, 58	llni2 37453	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝐹 ≠ 𝐺) → (𝐹 ∨ 𝐺) ∈ (LLines‘𝐾))
60	1, 52, 54, 57, 59	syl31anc 1371	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝐹 ∨ 𝐺) ∈ (LLines‘𝐾))
61	7, 8, 9, 10, 11, 18	cdlemeda 38239	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → 𝐷 ∈ 𝐴)
62	1, 3, 6, 42, 17, 38, 35, 61	syl223anc 1394	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐷 ∈ 𝐴)
63		simp23r 1293	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑇 ≤ 𝑊)
64	7, 8, 9, 10, 11, 25	cdlemeda 38239	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄))) → 𝑌 ∈ 𝐴)
65	1, 3, 21, 63, 17, 38, 36, 64	syl223anc 1394	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝑌 ∈ 𝐴)
66		simp32 1208	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)))
67		simp33l 1298	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))
68	7, 8, 9, 10, 11, 12, 13, 22, 18, 25, 39	cdleme20j 38259	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝐷 ≠ 𝑌)
69	47, 48, 49, 33, 31, 32, 34, 66, 67, 68	syl333anc 1400	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → 𝐷 ≠ 𝑌)
70	8, 10, 58	llni2 37453	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝐷 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝐷 ≠ 𝑌) → (𝐷 ∨ 𝑌) ∈ (LLines‘𝐾))
71	1, 62, 65, 69, 70	syl31anc 1371	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝐷 ∨ 𝑌) ∈ (LLines‘𝐾))
72		eqid 2738	. . . . . 6 ⊢ (LPlanes‘𝐾) = (LPlanes‘𝐾)
73	8, 9, 10, 58, 72	2llnmj 37501	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝐹 ∨ 𝐺) ∈ (LLines‘𝐾) ∧ (𝐷 ∨ 𝑌) ∈ (LLines‘𝐾)) → (((𝐹 ∨ 𝐺) ∧ (𝐷 ∨ 𝑌)) ∈ 𝐴 ↔ ((𝐹 ∨ 𝐺) ∨ (𝐷 ∨ 𝑌)) ∈ (LPlanes‘𝐾)))
74	1, 60, 71, 73	syl3anc 1369	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (((𝐹 ∨ 𝐺) ∧ (𝐷 ∨ 𝑌)) ∈ 𝐴 ↔ ((𝐹 ∨ 𝐺) ∨ (𝐷 ∨ 𝑌)) ∈ (LPlanes‘𝐾)))
75	46, 74	mpbid 231	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ((𝐹 ∨ 𝐺) ∨ (𝐷 ∨ 𝑌)) ∈ (LPlanes‘𝐾))
76	29, 75	eqeltrd 2839	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ((𝐹 ∨ 𝐷) ∨ (𝐺 ∨ 𝑌)) ∈ (LPlanes‘𝐾))
77	7, 8, 9, 10, 11, 12, 13, 22, 18, 25, 39	cdleme20l1 38261	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝐹 ∨ 𝐷) ∈ (LLines‘𝐾))
78	47, 48, 49, 17, 6, 42, 50, 35, 38, 77	syl333anc 1400	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝐹 ∨ 𝐷) ∈ (LLines‘𝐾))
79		eqid 2738	. . . . 5 ⊢ ((𝑇 ∨ 𝑆) ∧ 𝑊) = ((𝑇 ∨ 𝑆) ∧ 𝑊)
80	7, 8, 9, 10, 11, 12, 22, 13, 25, 18, 79	cdleme20l1 38261	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝐺 ∨ 𝑌) ∈ (LLines‘𝐾))
81	47, 48, 49, 17, 21, 63, 50, 36, 38, 80	syl333anc 1400	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (𝐺 ∨ 𝑌) ∈ (LLines‘𝐾))
82	8, 9, 10, 58, 72	2llnmj 37501	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝐹 ∨ 𝐷) ∈ (LLines‘𝐾) ∧ (𝐺 ∨ 𝑌) ∈ (LLines‘𝐾)) → (((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ 𝑌)) ∈ 𝐴 ↔ ((𝐹 ∨ 𝐷) ∨ (𝐺 ∨ 𝑌)) ∈ (LPlanes‘𝐾)))
83	1, 78, 81, 82	syl3anc 1369	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → (((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ 𝑌)) ∈ 𝐴 ↔ ((𝐹 ∨ 𝐷) ∨ (𝐺 ∨ 𝑌)) ∈ (LPlanes‘𝐾)))
84	76, 83	mpbird 256	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝑅 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇)))) → ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ 𝑌)) ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 Basecbs 16840 lecple 16895 joincjn 17944 meetcmee 17945 Latclat 18064 Atomscatm 37204 HLchlt 37291 LLinesclln 37432 LPlanesclpl 37433 LHypclh 37925

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-1st 7804 df-2nd 7805 df-proset 17928 df-poset 17946 df-plt 17963 df-lub 17979 df-glb 17980 df-join 17981 df-meet 17982 df-p0 18058 df-p1 18059 df-lat 18065 df-clat 18132 df-oposet 37117 df-ol 37119 df-oml 37120 df-covers 37207 df-ats 37208 df-atl 37239 df-cvlat 37263 df-hlat 37292 df-llines 37439 df-lplanes 37440 df-lvols 37441 df-lines 37442 df-psubsp 37444 df-pmap 37445 df-padd 37737 df-lhyp 37929

This theorem is referenced by: cdleme20l 38263

W3C validator