Proof of Theorem dalem5
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . 2
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 2 |  | dalemc.l | . 2
⊢  ≤ =
(le‘𝐾) | 
| 3 |  | dalema.ph | . . 3
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) | 
| 4 | 3 | dalemkelat 39626 | . 2
⊢ (𝜑 → 𝐾 ∈ Lat) | 
| 5 |  | dalemc.a | . . 3
⊢ 𝐴 = (Atoms‘𝐾) | 
| 6 | 3, 5 | dalemueb 39646 | . 2
⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾)) | 
| 7 | 3 | dalemkehl 39625 | . . 3
⊢ (𝜑 → 𝐾 ∈ HL) | 
| 8 | 3 | dalemrea 39630 | . . 3
⊢ (𝜑 → 𝑅 ∈ 𝐴) | 
| 9 |  | dalemc.j | . . . 4
⊢  ∨ =
(join‘𝐾) | 
| 10 |  | dalem5.o | . . . 4
⊢ 𝑂 = (LPlanes‘𝐾) | 
| 11 |  | dalem5.y | . . . 4
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) | 
| 12 | 3, 2, 9, 5, 10, 11 | dalemcea 39662 | . . 3
⊢ (𝜑 → 𝐶 ∈ 𝐴) | 
| 13 | 1, 9, 5 | hlatjcl 39368 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝑅 ∨ 𝐶) ∈ (Base‘𝐾)) | 
| 14 | 7, 8, 12, 13 | syl3anc 1373 | . 2
⊢ (𝜑 → (𝑅 ∨ 𝐶) ∈ (Base‘𝐾)) | 
| 15 |  | dalem5.w | . . 3
⊢ 𝑊 = (𝑌 ∨ 𝐶) | 
| 16 | 3, 10 | dalemyeb 39651 | . . . 4
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾)) | 
| 17 | 3, 5 | dalemceb 39640 | . . . 4
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾)) | 
| 18 | 1, 9 | latjcl 18484 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾)) → (𝑌 ∨ 𝐶) ∈ (Base‘𝐾)) | 
| 19 | 4, 16, 17, 18 | syl3anc 1373 | . . 3
⊢ (𝜑 → (𝑌 ∨ 𝐶) ∈ (Base‘𝐾)) | 
| 20 | 15, 19 | eqeltrid 2845 | . 2
⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾)) | 
| 21 | 3 | dalemclrju 39638 | . . 3
⊢ (𝜑 → 𝐶 ≤ (𝑅 ∨ 𝑈)) | 
| 22 | 3 | dalemuea 39633 | . . . 4
⊢ (𝜑 → 𝑈 ∈ 𝐴) | 
| 23 | 3 | dalempea 39628 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ 𝐴) | 
| 24 |  | simp313 1323 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) | 
| 25 | 3, 24 | sylbi 217 | . . . . 5
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) | 
| 26 | 2, 9, 5 | atnlej1 39381 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) → 𝐶 ≠ 𝑅) | 
| 27 | 7, 12, 8, 23, 25, 26 | syl131anc 1385 | . . . 4
⊢ (𝜑 → 𝐶 ≠ 𝑅) | 
| 28 | 2, 9, 5 | hlatexch1 39397 | . . . 4
⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝐶 ≠ 𝑅) → (𝐶 ≤ (𝑅 ∨ 𝑈) → 𝑈 ≤ (𝑅 ∨ 𝐶))) | 
| 29 | 7, 12, 22, 8, 27, 28 | syl131anc 1385 | . . 3
⊢ (𝜑 → (𝐶 ≤ (𝑅 ∨ 𝑈) → 𝑈 ≤ (𝑅 ∨ 𝐶))) | 
| 30 | 21, 29 | mpd 15 | . 2
⊢ (𝜑 → 𝑈 ≤ (𝑅 ∨ 𝐶)) | 
| 31 | 3, 9, 5 | dalempjqeb 39647 | . . . . . 6
⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) | 
| 32 | 3, 5 | dalemreb 39643 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ (Base‘𝐾)) | 
| 33 | 1, 2, 9 | latlej2 18494 | . . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) | 
| 34 | 4, 31, 32, 33 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) | 
| 35 | 34, 11 | breqtrrdi 5185 | . . . 4
⊢ (𝜑 → 𝑅 ≤ 𝑌) | 
| 36 | 1, 2, 9 | latjlej1 18498 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾))) → (𝑅 ≤ 𝑌 → (𝑅 ∨ 𝐶) ≤ (𝑌 ∨ 𝐶))) | 
| 37 | 4, 32, 16, 17, 36 | syl13anc 1374 | . . . 4
⊢ (𝜑 → (𝑅 ≤ 𝑌 → (𝑅 ∨ 𝐶) ≤ (𝑌 ∨ 𝐶))) | 
| 38 | 35, 37 | mpd 15 | . . 3
⊢ (𝜑 → (𝑅 ∨ 𝐶) ≤ (𝑌 ∨ 𝐶)) | 
| 39 | 38, 15 | breqtrrdi 5185 | . 2
⊢ (𝜑 → (𝑅 ∨ 𝐶) ≤ 𝑊) | 
| 40 | 1, 2, 4, 6, 14, 20, 30, 39 | lattrd 18491 | 1
⊢ (𝜑 → 𝑈 ≤ 𝑊) |