Metamath Proof Explorer

Theorem dalem44

Description: Lemma for dath . Dummy center of perspectivity c lies outside of plane G H I . (Contributed by NM, 16-Aug-2012)

Ref Expression
Hypotheses dalem.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
dalem.l ⊢ ≤ = ( le ‘ 𝐾 )
dalem.j ⊢ ∨ = ( join ‘ 𝐾 )
dalem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dalem.ps ⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
dalem44.m ⊢ ∧ = ( meet ‘ 𝐾 )
dalem44.o ⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
dalem44.y ⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
dalem44.z ⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
dalem44.g ⊢ 𝐺 = ( ( 𝑐 ∨ 𝑃 ) ∧ ( 𝑑 ∨ 𝑆 ) )
dalem44.h ⊢ 𝐻 = ( ( 𝑐 ∨ 𝑄 ) ∧ ( 𝑑 ∨ 𝑇 ) )
dalem44.i ⊢ 𝐼 = ( ( 𝑐 ∨ 𝑅 ) ∧ ( 𝑑 ∨ 𝑈 ) )
Assertion dalem44 ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ¬ 𝑐 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 dalem.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
2 dalem.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dalem.j ⊢ ∨ = ( join ‘ 𝐾 )
4 dalem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dalem.ps ⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
6 dalem44.m ⊢ ∧ = ( meet ‘ 𝐾 )
7 dalem44.o ⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
8 dalem44.y ⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
9 dalem44.z ⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
10 dalem44.g ⊢ 𝐺 = ( ( 𝑐 ∨ 𝑃 ) ∧ ( 𝑑 ∨ 𝑆 ) )
11 dalem44.h ⊢ 𝐻 = ( ( 𝑐 ∨ 𝑄 ) ∧ ( 𝑑 ∨ 𝑇 ) )
12 dalem44.i ⊢ 𝐼 = ( ( 𝑐 ∨ 𝑅 ) ∧ ( 𝑑 ∨ 𝑈 ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 dalem43 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ≠ 𝑌 )
14 13 necomd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑌 ≠ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) )
15 1 dalemkelat ⊢ ( 𝜑 → 𝐾 ∈ Lat )
16 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐾 ∈ Lat )
17 5 4 dalemcceb ⊢ ( 𝜓 → 𝑐 ∈ ( Base ‘ 𝐾 ) )
18 17 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑐 ∈ ( Base ‘ 𝐾 ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 dalem42 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ∈ 𝑂 )
20 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21 20 7 lplnbase ⊢ ( ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ∈ 𝑂 → ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ∈ ( Base ‘ 𝐾 ) )
22 19 21 syl ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ∈ ( Base ‘ 𝐾 ) )
23 20 2 3 latleeqj1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑐 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑐 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ↔ ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) = ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
24 16 18 22 23 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ↔ ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) = ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
25 1 2 3 4 5 6 7 8 9 10 dalem28 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑃 ≤ ( 𝐺 ∨ 𝑐 ) )
26 1 dalemkehl ⊢ ( 𝜑 → 𝐾 ∈ HL )
27 26 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐾 ∈ HL )
28 5 dalemccea ⊢ ( 𝜓 → 𝑐 ∈ 𝐴 )
29 28 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑐 ∈ 𝐴 )
30 1 2 3 4 5 6 7 8 9 10 dalem23 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐺 ∈ 𝐴 )
31 3 4 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑐 ∨ 𝐺 ) = ( 𝐺 ∨ 𝑐 ) )
32 27 29 30 31 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝐺 ) = ( 𝐺 ∨ 𝑐 ) )
33 25 32 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑃 ≤ ( 𝑐 ∨ 𝐺 ) )
34 1 2 3 4 5 6 7 8 9 11 dalem33 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑄 ≤ ( 𝐻 ∨ 𝑐 ) )
35 1 2 3 4 5 6 7 8 9 11 dalem29 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐻 ∈ 𝐴 )
36 3 4 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ) → ( 𝑐 ∨ 𝐻 ) = ( 𝐻 ∨ 𝑐 ) )
37 27 29 35 36 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝐻 ) = ( 𝐻 ∨ 𝑐 ) )
38 34 37 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑄 ≤ ( 𝑐 ∨ 𝐻 ) )
39 1 4 dalempeb ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
40 39 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
41 20 3 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑐 ∨ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
42 27 29 30 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
43 1 4 dalemqeb ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
44 43 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
45 20 3 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ) → ( 𝑐 ∨ 𝐻 ) ∈ ( Base ‘ 𝐾 ) )
46 27 29 35 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝐻 ) ∈ ( Base ‘ 𝐾 ) )
47 20 2 3 latjlej12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑐 ∨ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑐 ∨ 𝐻 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( 𝑐 ∨ 𝐺 ) ∧ 𝑄 ≤ ( 𝑐 ∨ 𝐻 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑐 ∨ 𝐺 ) ∨ ( 𝑐 ∨ 𝐻 ) ) ) )
48 16 40 42 44 46 47 syl122anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑃 ≤ ( 𝑐 ∨ 𝐺 ) ∧ 𝑄 ≤ ( 𝑐 ∨ 𝐻 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑐 ∨ 𝐺 ) ∨ ( 𝑐 ∨ 𝐻 ) ) ) )
49 33 38 48 mp2and ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑐 ∨ 𝐺 ) ∨ ( 𝑐 ∨ 𝐻 ) ) )
50 20 4 atbase ⊢ ( 𝐺 ∈ 𝐴 → 𝐺 ∈ ( Base ‘ 𝐾 ) )
51 30 50 syl ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐺 ∈ ( Base ‘ 𝐾 ) )
52 20 4 atbase ⊢ ( 𝐻 ∈ 𝐴 → 𝐻 ∈ ( Base ‘ 𝐾 ) )
53 35 52 syl ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐻 ∈ ( Base ‘ 𝐾 ) )
54 20 3 latjjdi ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑐 ∈ ( Base ‘ 𝐾 ) ∧ 𝐺 ∈ ( Base ‘ 𝐾 ) ∧ 𝐻 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) = ( ( 𝑐 ∨ 𝐺 ) ∨ ( 𝑐 ∨ 𝐻 ) ) )
55 16 18 51 53 54 syl13anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) = ( ( 𝑐 ∨ 𝐺 ) ∨ ( 𝑐 ∨ 𝐻 ) ) )
56 49 55 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) )
57 1 2 3 4 5 6 7 8 9 12 dalem37 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑅 ≤ ( 𝐼 ∨ 𝑐 ) )
58 1 2 3 4 5 6 7 8 9 12 dalem34 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐼 ∈ 𝐴 )
59 3 4 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝐼 ∈ 𝐴 ) → ( 𝑐 ∨ 𝐼 ) = ( 𝐼 ∨ 𝑐 ) )
60 27 29 58 59 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝐼 ) = ( 𝐼 ∨ 𝑐 ) )
61 57 60 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑅 ≤ ( 𝑐 ∨ 𝐼 ) )
62 1 3 4 dalempjqeb ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
63 62 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
64 20 3 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ) → ( 𝐺 ∨ 𝐻 ) ∈ ( Base ‘ 𝐾 ) )
65 27 30 35 64 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝐺 ∨ 𝐻 ) ∈ ( Base ‘ 𝐾 ) )
66 20 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑐 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ∨ 𝐻 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∈ ( Base ‘ 𝐾 ) )
67 16 18 65 66 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∈ ( Base ‘ 𝐾 ) )
68 1 4 dalemreb ⊢ ( 𝜑 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
69 68 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
70 20 3 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝐼 ∈ 𝐴 ) → ( 𝑐 ∨ 𝐼 ) ∈ ( Base ‘ 𝐾 ) )
71 27 29 58 70 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝐼 ) ∈ ( Base ‘ 𝐾 ) )
72 20 2 3 latjlej12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑐 ∨ 𝐼 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∧ 𝑅 ≤ ( 𝑐 ∨ 𝐼 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∨ ( 𝑐 ∨ 𝐼 ) ) ) )
73 16 63 67 69 71 72 syl122anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∧ 𝑅 ≤ ( 𝑐 ∨ 𝐼 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∨ ( 𝑐 ∨ 𝐼 ) ) ) )
74 56 61 73 mp2and ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∨ ( 𝑐 ∨ 𝐼 ) ) )
75 20 4 atbase ⊢ ( 𝐼 ∈ 𝐴 → 𝐼 ∈ ( Base ‘ 𝐾 ) )
76 58 75 syl ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐼 ∈ ( Base ‘ 𝐾 ) )
77 20 3 latjjdi ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑐 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ∨ 𝐻 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝐼 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) = ( ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∨ ( 𝑐 ∨ 𝐼 ) ) )
78 16 18 65 76 77 syl13anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) = ( ( 𝑐 ∨ ( 𝐺 ∨ 𝐻 ) ) ∨ ( 𝑐 ∨ 𝐼 ) ) )
79 74 78 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
80 8 79 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑌 ≤ ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
81 breq2 ⊢ ( ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) = ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) → ( 𝑌 ≤ ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) ↔ 𝑌 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
82 80 81 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) = ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) → 𝑌 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
83 24 82 sylbid ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) → 𝑌 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
84 1 dalemyeo ⊢ ( 𝜑 → 𝑌 ∈ 𝑂 )
85 84 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑌 ∈ 𝑂 )
86 2 7 lplncmp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑂 ∧ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ∈ 𝑂 ) → ( 𝑌 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ↔ 𝑌 = ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
87 27 85 19 86 syl3anc ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑌 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ↔ 𝑌 = ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
88 83 87 sylibd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) → 𝑌 = ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
89 88 necon3ad ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑌 ≠ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) → ¬ 𝑐 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) ) )
90 14 89 mpd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ¬ 𝑐 ≤ ( ( 𝐺 ∨ 𝐻 ) ∨ 𝐼 ) )