Theorem dalem-cly 40478

Description: Lemma for dalem9 40479. Center of perspectivity 𝐶 is not in plane 𝑌 (when 𝑌 and 𝑍 are different planes). (Contributed by NM, 13-Aug-2012.)

Hypotheses

Ref	Expression
dalema.ph	⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
dalemc.l	⊢ ≤ = (le‘𝐾)
dalemc.j	⊢ ∨ = (join‘𝐾)
dalemc.a	⊢ 𝐴 = (Atoms‘𝐾)
dalem-cly.o	⊢ 𝑂 = (LPlanes‘𝐾)
dalem-cly.y	⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
dalem-cly.z	⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)

Assertion

Ref	Expression
dalem-cly	⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → ¬ 𝐶 ≤ 𝑌)

Proof of Theorem dalem-cly

Step	Hyp	Ref	Expression
1		dalema.ph	. . . . . . 7 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
2	1	dalemkelat 40431	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ Lat)
3		dalemc.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
4	1, 3	dalemceb 40445	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾))
5		dalem-cly.o	. . . . . . 7 ⊢ 𝑂 = (LPlanes‘𝐾)
6	1, 5	dalemyeb 40456	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾))
7		eqid 2766	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
8		dalemc.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
9		dalemc.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
10	7, 8, 9	latleeqj1 18532	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝐶 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝐶 ≤ 𝑌 ↔ (𝐶 ∨ 𝑌) = 𝑌))
11	2, 4, 6, 10	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (𝐶 ≤ 𝑌 ↔ (𝐶 ∨ 𝑌) = 𝑌))
12	1	dalemclpjs 40441	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ≤ (𝑃 ∨ 𝑆))
13	1	dalemkehl 40430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ HL)
14		dalem-cly.y	. . . . . . . . . . . . . . 15 ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
15	1, 8, 9, 3, 5, 14	dalemcea 40467	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
16	1	dalemsea 40436	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ 𝐴)
17	1	dalempea 40433	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
18	1	dalemqea 40434	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
19	1	dalem-clpjq 40444	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝐶 ≤ (𝑃 ∨ 𝑄))
20	8, 9, 3	atnlej1 40186	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) → 𝐶 ≠ 𝑃)
21	13, 15, 17, 18, 19, 20	syl131anc 1410	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ≠ 𝑃)
22	8, 9, 3	hlatexch1 40202	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝐶 ≠ 𝑃) → (𝐶 ≤ (𝑃 ∨ 𝑆) → 𝑆 ≤ (𝑃 ∨ 𝐶)))
23	13, 15, 16, 17, 21, 22	syl131anc 1410	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 ≤ (𝑃 ∨ 𝑆) → 𝑆 ≤ (𝑃 ∨ 𝐶)))
24	12, 23	mpd 16	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ≤ (𝑃 ∨ 𝐶))
25	9, 3	hlatjcom 40175	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝐶 ∨ 𝑃) = (𝑃 ∨ 𝐶))
26	13, 15, 17, 25	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∨ 𝑃) = (𝑃 ∨ 𝐶))
27	24, 26	breqtrrd 5144	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ≤ (𝐶 ∨ 𝑃))
28	1	dalemclqjt 40442	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ≤ (𝑄 ∨ 𝑇))
29	1	dalemtea 40437	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ 𝐴)
30	1	dalemrea 40435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ 𝐴)
31		simp312 1340	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑄 ∨ 𝑅))
32	1, 31	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝐶 ≤ (𝑄 ∨ 𝑅))
33	8, 9, 3	atnlej1 40186	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅)) → 𝐶 ≠ 𝑄)
34	13, 15, 18, 30, 32, 33	syl131anc 1410	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ≠ 𝑄)
35	8, 9, 3	hlatexch1 40202	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝐶 ≠ 𝑄) → (𝐶 ≤ (𝑄 ∨ 𝑇) → 𝑇 ≤ (𝑄 ∨ 𝐶)))
36	13, 15, 29, 18, 34, 35	syl131anc 1410	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 ≤ (𝑄 ∨ 𝑇) → 𝑇 ≤ (𝑄 ∨ 𝐶)))
37	28, 36	mpd 16	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ≤ (𝑄 ∨ 𝐶))
38	9, 3	hlatjcom 40175	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝐶 ∨ 𝑄) = (𝑄 ∨ 𝐶))
39	13, 15, 18, 38	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∨ 𝑄) = (𝑄 ∨ 𝐶))
40	37, 39	breqtrrd 5144	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ≤ (𝐶 ∨ 𝑄))
41	1, 3	dalemseb 40449	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (Base‘𝐾))
42	7, 9, 3	hlatjcl 40174	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝐶 ∨ 𝑃) ∈ (Base‘𝐾))
43	13, 15, 17, 42	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∨ 𝑃) ∈ (Base‘𝐾))
44	1, 3	dalemteb 40450	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ (Base‘𝐾))
45	7, 9, 3	hlatjcl 40174	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝐶 ∨ 𝑄) ∈ (Base‘𝐾))
46	13, 15, 18, 45	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∨ 𝑄) ∈ (Base‘𝐾))
47	7, 8, 9	latjlej12 18536	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝐶 ∨ 𝑃) ∈ (Base‘𝐾)) ∧ (𝑇 ∈ (Base‘𝐾) ∧ (𝐶 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑆 ≤ (𝐶 ∨ 𝑃) ∧ 𝑇 ≤ (𝐶 ∨ 𝑄)) → (𝑆 ∨ 𝑇) ≤ ((𝐶 ∨ 𝑃) ∨ (𝐶 ∨ 𝑄))))
48	2, 41, 43, 44, 46, 47	syl122anc 1406	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑆 ≤ (𝐶 ∨ 𝑃) ∧ 𝑇 ≤ (𝐶 ∨ 𝑄)) → (𝑆 ∨ 𝑇) ≤ ((𝐶 ∨ 𝑃) ∨ (𝐶 ∨ 𝑄))))
49	27, 40, 48	mp2and 712	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ∨ 𝑇) ≤ ((𝐶 ∨ 𝑃) ∨ (𝐶 ∨ 𝑄)))
50	1, 3	dalempeb 40446	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝐾))
51	1, 3	dalemqeb 40447	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝐾))
52	7, 9	latjjdi 18572	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝐶 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾))) → (𝐶 ∨ (𝑃 ∨ 𝑄)) = ((𝐶 ∨ 𝑃) ∨ (𝐶 ∨ 𝑄)))
53	2, 4, 50, 51, 52	syl13anc 1399	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ∨ (𝑃 ∨ 𝑄)) = ((𝐶 ∨ 𝑃) ∨ (𝐶 ∨ 𝑄)))
54	49, 53	breqtrrd 5144	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ∨ 𝑇) ≤ (𝐶 ∨ (𝑃 ∨ 𝑄)))
55	1	dalemclrju 40443	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ≤ (𝑅 ∨ 𝑈))
56	1	dalemuea 40438	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
57		simp313 1341	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃))
58	1, 57	sylbi 220	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃))
59	8, 9, 3	atnlej1 40186	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) → 𝐶 ≠ 𝑅)
60	13, 15, 30, 17, 58, 59	syl131anc 1410	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ≠ 𝑅)
61	8, 9, 3	hlatexch1 40202	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝐶 ≠ 𝑅) → (𝐶 ≤ (𝑅 ∨ 𝑈) → 𝑈 ≤ (𝑅 ∨ 𝐶)))
62	13, 15, 56, 30, 60, 61	syl131anc 1410	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ≤ (𝑅 ∨ 𝑈) → 𝑈 ≤ (𝑅 ∨ 𝐶)))
63	55, 62	mpd 16	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ≤ (𝑅 ∨ 𝐶))
64	9, 3	hlatjcom 40175	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝐶 ∨ 𝑅) = (𝑅 ∨ 𝐶))
65	13, 15, 30, 64	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ∨ 𝑅) = (𝑅 ∨ 𝐶))
66	63, 65	breqtrrd 5144	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ≤ (𝐶 ∨ 𝑅))
67	1, 9, 3	dalemsjteb 40453	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
68	1, 9, 3	dalempjqeb 40452	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
69	7, 9	latjcl 18520	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝐶 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝐶 ∨ (𝑃 ∨ 𝑄)) ∈ (Base‘𝐾))
70	2, 4, 68, 69	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ∨ (𝑃 ∨ 𝑄)) ∈ (Base‘𝐾))
71	1, 3	dalemueb 40451	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
72	7, 9, 3	hlatjcl 40174	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝐶 ∨ 𝑅) ∈ (Base‘𝐾))
73	13, 15, 30, 72	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ∨ 𝑅) ∈ (Base‘𝐾))
74	7, 8, 9	latjlej12 18536	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ ((𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝐶 ∨ (𝑃 ∨ 𝑄)) ∈ (Base‘𝐾)) ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝐶 ∨ 𝑅) ∈ (Base‘𝐾))) → (((𝑆 ∨ 𝑇) ≤ (𝐶 ∨ (𝑃 ∨ 𝑄)) ∧ 𝑈 ≤ (𝐶 ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝐶 ∨ (𝑃 ∨ 𝑄)) ∨ (𝐶 ∨ 𝑅))))
75	2, 67, 70, 71, 73, 74	syl122anc 1406	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆 ∨ 𝑇) ≤ (𝐶 ∨ (𝑃 ∨ 𝑄)) ∧ 𝑈 ≤ (𝐶 ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝐶 ∨ (𝑃 ∨ 𝑄)) ∨ (𝐶 ∨ 𝑅))))
76	54, 66, 75	mp2and 712	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝐶 ∨ (𝑃 ∨ 𝑄)) ∨ (𝐶 ∨ 𝑅)))
77	1, 3	dalemreb 40448	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ (Base‘𝐾))
78	7, 9	latjjdi 18572	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝐶 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾))) → (𝐶 ∨ ((𝑃 ∨ 𝑄) ∨ 𝑅)) = ((𝐶 ∨ (𝑃 ∨ 𝑄)) ∨ (𝐶 ∨ 𝑅)))
79	2, 4, 68, 77, 78	syl13anc 1399	. . . . . . . 8 ⊢ (𝜑 → (𝐶 ∨ ((𝑃 ∨ 𝑄) ∨ 𝑅)) = ((𝐶 ∨ (𝑃 ∨ 𝑄)) ∨ (𝐶 ∨ 𝑅)))
80	76, 79	breqtrrd 5144	. . . . . . 7 ⊢ (𝜑 → ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ (𝐶 ∨ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
81		dalem-cly.z	. . . . . . 7 ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)
82	14	oveq2i 7434	. . . . . . 7 ⊢ (𝐶 ∨ 𝑌) = (𝐶 ∨ ((𝑃 ∨ 𝑄) ∨ 𝑅))
83	80, 81, 82	3brtr4g 5150	. . . . . 6 ⊢ (𝜑 → 𝑍 ≤ (𝐶 ∨ 𝑌))
84		breq2 5118	. . . . . 6 ⊢ ((𝐶 ∨ 𝑌) = 𝑌 → (𝑍 ≤ (𝐶 ∨ 𝑌) ↔ 𝑍 ≤ 𝑌))
85	83, 84	syl5ibcom 248	. . . . 5 ⊢ (𝜑 → ((𝐶 ∨ 𝑌) = 𝑌 → 𝑍 ≤ 𝑌))
86	11, 85	sylbid 243	. . . 4 ⊢ (𝜑 → (𝐶 ≤ 𝑌 → 𝑍 ≤ 𝑌))
87	1	dalemzeo 40440	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑂)
88	1	dalemyeo 40439	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑂)
89	8, 5	lplncmp 40369	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑍 ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) → (𝑍 ≤ 𝑌 ↔ 𝑍 = 𝑌))
90	13, 87, 88, 89	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (𝑍 ≤ 𝑌 ↔ 𝑍 = 𝑌))
91		eqcom 2773	. . . . 5 ⊢ (𝑍 = 𝑌 ↔ 𝑌 = 𝑍)
92	90, 91	bitrdi 290	. . . 4 ⊢ (𝜑 → (𝑍 ≤ 𝑌 ↔ 𝑌 = 𝑍))
93	86, 92	sylibd 242	. . 3 ⊢ (𝜑 → (𝐶 ≤ 𝑌 → 𝑌 = 𝑍))
94	93	necon3ad 2974	. 2 ⊢ (𝜑 → (𝑌 ≠ 𝑍 → ¬ 𝐶 ≤ 𝑌))
95	94	imp 412	1 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → ¬ 𝐶 ≤ 𝑌)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2961   class class class wbr 5114  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  lecple 17342  joincjn 18392  Latclat 18512  Atomscatm 40070  HLchlt 40157  LPlanesclpl 40299

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-proset 18375  df-poset 18394  df-plt 18409  df-lub 18425  df-glb 18426  df-join 18427  df-meet 18428  df-p0 18504  df-lat 18513  df-clat 18580  df-oposet 39983  df-ol 39985  df-oml 39986  df-covers 40073  df-ats 40074  df-atl 40105  df-cvlat 40129  df-hlat 40158  df-llines 40305  df-lplanes 40306

This theorem is used by:  dalem9  40479