This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝑌 ≠ 𝑍 ) → ¬ 𝐶 ≤ 𝑌 )