Theorem dalem-cly

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

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

Proof

Step	Hyp	Ref	Expression
1		dalema.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
2		dalemc.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dalemc.j	⊢ ∨ = ( join ‘ 𝐾 )
4		dalemc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dalem-cly.o	⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
6		dalem-cly.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
7		dalem-cly.z	⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
8	1	dalemkelat	⊢ ( 𝜑 → 𝐾 ∈ Lat )
9	1 4	dalemceb	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐾 ) )
10	1 5	dalemyeb	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 2 3	latleeqj1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐶 ≤ 𝑌 ↔ ( 𝐶 ∨ 𝑌 ) = 𝑌 ) )
13	8 9 10 12	syl3anc	⊢ ( 𝜑 → ( 𝐶 ≤ 𝑌 ↔ ( 𝐶 ∨ 𝑌 ) = 𝑌 ) )
14	1	dalemclpjs	⊢ ( 𝜑 → 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) )
15	1	dalemkehl	⊢ ( 𝜑 → 𝐾 ∈ HL )
16	1 2 3 4 5 6	dalemcea	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
17	1	dalemsea	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
18	1	dalempea	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
19	1	dalemqea	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
20	1	dalem-clpjq	⊢ ( 𝜑 → ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) )
21	2 3 4	atnlej1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐶 ≠ 𝑃 )
22	15 16 18 19 20 21	syl131anc	⊢ ( 𝜑 → 𝐶 ≠ 𝑃 )
23	2 3 4	hlatexch1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝐶 ≠ 𝑃 ) → ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) → 𝑆 ≤ ( 𝑃 ∨ 𝐶 ) ) )
24	15 16 17 18 22 23	syl131anc	⊢ ( 𝜑 → ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) → 𝑆 ≤ ( 𝑃 ∨ 𝐶 ) ) )
25	14 24	mpd	⊢ ( 𝜑 → 𝑆 ≤ ( 𝑃 ∨ 𝐶 ) )
26	3 4	hlatjcom	⊢ ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐶 ∨ 𝑃 ) = ( 𝑃 ∨ 𝐶 ) )
27	15 16 18 26	syl3anc	⊢ ( 𝜑 → ( 𝐶 ∨ 𝑃 ) = ( 𝑃 ∨ 𝐶 ) )
28	25 27	breqtrrd	⊢ ( 𝜑 → 𝑆 ≤ ( 𝐶 ∨ 𝑃 ) )
29	1	dalemclqjt	⊢ ( 𝜑 → 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) )
30	1	dalemtea	⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
31	1	dalemrea	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
32		simp312	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) → ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) )
33	1 32	sylbi	⊢ ( 𝜑 → ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) )
34	2 3 4	atnlej1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝐶 ≠ 𝑄 )
35	15 16 19 31 33 34	syl131anc	⊢ ( 𝜑 → 𝐶 ≠ 𝑄 )
36	2 3 4	hlatexch1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝐶 ≠ 𝑄 ) → ( 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) → 𝑇 ≤ ( 𝑄 ∨ 𝐶 ) ) )
37	15 16 30 19 35 36	syl131anc	⊢ ( 𝜑 → ( 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) → 𝑇 ≤ ( 𝑄 ∨ 𝐶 ) ) )
38	29 37	mpd	⊢ ( 𝜑 → 𝑇 ≤ ( 𝑄 ∨ 𝐶 ) )
39	3 4	hlatjcom	⊢ ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝐶 ∨ 𝑄 ) = ( 𝑄 ∨ 𝐶 ) )
40	15 16 19 39	syl3anc	⊢ ( 𝜑 → ( 𝐶 ∨ 𝑄 ) = ( 𝑄 ∨ 𝐶 ) )
41	38 40	breqtrrd	⊢ ( 𝜑 → 𝑇 ≤ ( 𝐶 ∨ 𝑄 ) )
42	1 4	dalemseb	⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
43	11 3 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐶 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
44	15 16 18 43	syl3anc	⊢ ( 𝜑 → ( 𝐶 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
45	1 4	dalemteb	⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
46	11 3 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝐶 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
47	15 16 19 46	syl3anc	⊢ ( 𝜑 → ( 𝐶 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
48	11 2 3	latjlej12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐶 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐶 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ ( 𝐶 ∨ 𝑃 ) ∧ 𝑇 ≤ ( 𝐶 ∨ 𝑄 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝐶 ∨ 𝑃 ) ∨ ( 𝐶 ∨ 𝑄 ) ) ) )
49	8 42 44 45 47 48	syl122anc	⊢ ( 𝜑 → ( ( 𝑆 ≤ ( 𝐶 ∨ 𝑃 ) ∧ 𝑇 ≤ ( 𝐶 ∨ 𝑄 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝐶 ∨ 𝑃 ) ∨ ( 𝐶 ∨ 𝑄 ) ) ) )
50	28 41 49	mp2and	⊢ ( 𝜑 → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝐶 ∨ 𝑃 ) ∨ ( 𝐶 ∨ 𝑄 ) ) )
51	1 4	dalempeb	⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
52	1 4	dalemqeb	⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
53	11 3	latjjdi	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝐶 ∨ 𝑃 ) ∨ ( 𝐶 ∨ 𝑄 ) ) )
54	8 9 51 52 53	syl13anc	⊢ ( 𝜑 → ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝐶 ∨ 𝑃 ) ∨ ( 𝐶 ∨ 𝑄 ) ) )
55	50 54	breqtrrd	⊢ ( 𝜑 → ( 𝑆 ∨ 𝑇 ) ≤ ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) )
56	1	dalemclrju	⊢ ( 𝜑 → 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) )
57	1	dalemuea	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
58		simp313	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) → ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) )
59	1 58	sylbi	⊢ ( 𝜑 → ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) )
60	2 3 4	atnlej1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) → 𝐶 ≠ 𝑅 )
61	15 16 31 18 59 60	syl131anc	⊢ ( 𝜑 → 𝐶 ≠ 𝑅 )
62	2 3 4	hlatexch1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝐶 ≠ 𝑅 ) → ( 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) → 𝑈 ≤ ( 𝑅 ∨ 𝐶 ) ) )
63	15 16 57 31 61 62	syl131anc	⊢ ( 𝜑 → ( 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) → 𝑈 ≤ ( 𝑅 ∨ 𝐶 ) ) )
64	56 63	mpd	⊢ ( 𝜑 → 𝑈 ≤ ( 𝑅 ∨ 𝐶 ) )
65	3 4	hlatjcom	⊢ ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝐶 ∨ 𝑅 ) = ( 𝑅 ∨ 𝐶 ) )
66	15 16 31 65	syl3anc	⊢ ( 𝜑 → ( 𝐶 ∨ 𝑅 ) = ( 𝑅 ∨ 𝐶 ) )
67	64 66	breqtrrd	⊢ ( 𝜑 → 𝑈 ≤ ( 𝐶 ∨ 𝑅 ) )
68	1 3 4	dalemsjteb	⊢ ( 𝜑 → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
69	1 3 4	dalempjqeb	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
70	11 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
71	8 9 69 70	syl3anc	⊢ ( 𝜑 → ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
72	1 4	dalemueb	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
73	11 3 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝐶 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
74	15 16 31 73	syl3anc	⊢ ( 𝜑 → ( 𝐶 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
75	11 2 3	latjlej12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐶 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ ( 𝐶 ∨ 𝑅 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∨ ( 𝐶 ∨ 𝑅 ) ) ) )
76	8 68 71 72 74 75	syl122anc	⊢ ( 𝜑 → ( ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ ( 𝐶 ∨ 𝑅 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∨ ( 𝐶 ∨ 𝑅 ) ) ) )
77	55 67 76	mp2and	⊢ ( 𝜑 → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∨ ( 𝐶 ∨ 𝑅 ) ) )
78	1 4	dalemreb	⊢ ( 𝜑 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
79	11 3	latjjdi	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐶 ∨ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) = ( ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∨ ( 𝐶 ∨ 𝑅 ) ) )
80	8 9 69 78 79	syl13anc	⊢ ( 𝜑 → ( 𝐶 ∨ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) = ( ( 𝐶 ∨ ( 𝑃 ∨ 𝑄 ) ) ∨ ( 𝐶 ∨ 𝑅 ) ) )
81	77 80	breqtrrd	⊢ ( 𝜑 → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ ( 𝐶 ∨ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
82	6	oveq2i	⊢ ( 𝐶 ∨ 𝑌 ) = ( 𝐶 ∨ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
83	81 7 82	3brtr4g	⊢ ( 𝜑 → 𝑍 ≤ ( 𝐶 ∨ 𝑌 ) )
84		breq2	⊢ ( ( 𝐶 ∨ 𝑌 ) = 𝑌 → ( 𝑍 ≤ ( 𝐶 ∨ 𝑌 ) ↔ 𝑍 ≤ 𝑌 ) )
85	83 84	syl5ibcom	⊢ ( 𝜑 → ( ( 𝐶 ∨ 𝑌 ) = 𝑌 → 𝑍 ≤ 𝑌 ) )
86	13 85	sylbid	⊢ ( 𝜑 → ( 𝐶 ≤ 𝑌 → 𝑍 ≤ 𝑌 ) )
87	1	dalemzeo	⊢ ( 𝜑 → 𝑍 ∈ 𝑂 )
88	1	dalemyeo	⊢ ( 𝜑 → 𝑌 ∈ 𝑂 )
89	2 5	lplncmp	⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ∈ 𝑂 ∧ 𝑌 ∈ 𝑂 ) → ( 𝑍 ≤ 𝑌 ↔ 𝑍 = 𝑌 ) )
90	15 87 88 89	syl3anc	⊢ ( 𝜑 → ( 𝑍 ≤ 𝑌 ↔ 𝑍 = 𝑌 ) )
91		eqcom	⊢ ( 𝑍 = 𝑌 ↔ 𝑌 = 𝑍 )
92	90 91	bitrdi	⊢ ( 𝜑 → ( 𝑍 ≤ 𝑌 ↔ 𝑌 = 𝑍 ) )
93	86 92	sylibd	⊢ ( 𝜑 → ( 𝐶 ≤ 𝑌 → 𝑌 = 𝑍 ) )
94	93	necon3ad	⊢ ( 𝜑 → ( 𝑌 ≠ 𝑍 → ¬ 𝐶 ≤ 𝑌 ) )
95	94	imp	⊢ ( ( 𝜑 ∧ 𝑌 ≠ 𝑍 ) → ¬ 𝐶 ≤ 𝑌 )