Proof of Theorem dalemrot
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dalema.ph | . . . . 5
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) | 
| 2 | 1 | dalemkehl 39625 | . . . 4
⊢ (𝜑 → 𝐾 ∈ HL) | 
| 3 |  | dalemc.a | . . . . 5
⊢ 𝐴 = (Atoms‘𝐾) | 
| 4 | 1, 3 | dalemceb 39640 | . . . 4
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾)) | 
| 5 | 2, 4 | jca 511 | . . 3
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾))) | 
| 6 | 1 | dalemqea 39629 | . . . 4
⊢ (𝜑 → 𝑄 ∈ 𝐴) | 
| 7 | 1 | dalemrea 39630 | . . . 4
⊢ (𝜑 → 𝑅 ∈ 𝐴) | 
| 8 | 1 | dalempea 39628 | . . . 4
⊢ (𝜑 → 𝑃 ∈ 𝐴) | 
| 9 | 6, 7, 8 | 3jca 1129 | . . 3
⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴)) | 
| 10 | 1 | dalemtea 39632 | . . . 4
⊢ (𝜑 → 𝑇 ∈ 𝐴) | 
| 11 | 1 | dalemuea 39633 | . . . 4
⊢ (𝜑 → 𝑈 ∈ 𝐴) | 
| 12 | 1 | dalemsea 39631 | . . . 4
⊢ (𝜑 → 𝑆 ∈ 𝐴) | 
| 13 | 10, 11, 12 | 3jca 1129 | . . 3
⊢ (𝜑 → (𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) | 
| 14 | 5, 9, 13 | 3jca 1129 | . 2
⊢ (𝜑 → ((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ (𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))) | 
| 15 |  | dalemc.j | . . . . 5
⊢  ∨ =
(join‘𝐾) | 
| 16 | 1, 15, 3 | dalemqrprot 39650 | . . . 4
⊢ (𝜑 → ((𝑄 ∨ 𝑅) ∨ 𝑃) = ((𝑃 ∨ 𝑄) ∨ 𝑅)) | 
| 17 |  | dalemrot.y | . . . . 5
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) | 
| 18 | 1 | dalemyeo 39634 | . . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑂) | 
| 19 | 17, 18 | eqeltrrid 2846 | . . . 4
⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂) | 
| 20 | 16, 19 | eqeltrd 2841 | . . 3
⊢ (𝜑 → ((𝑄 ∨ 𝑅) ∨ 𝑃) ∈ 𝑂) | 
| 21 | 15, 3 | hlatjrot 39374 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑇 ∨ 𝑈) ∨ 𝑆) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) | 
| 22 | 2, 10, 11, 12, 21 | syl13anc 1374 | . . . 4
⊢ (𝜑 → ((𝑇 ∨ 𝑈) ∨ 𝑆) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) | 
| 23 |  | dalemrot.z | . . . . 5
⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) | 
| 24 | 1 | dalemzeo 39635 | . . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑂) | 
| 25 | 23, 24 | eqeltrrid 2846 | . . . 4
⊢ (𝜑 → ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂) | 
| 26 | 22, 25 | eqeltrd 2841 | . . 3
⊢ (𝜑 → ((𝑇 ∨ 𝑈) ∨ 𝑆) ∈ 𝑂) | 
| 27 | 20, 26 | jca 511 | . 2
⊢ (𝜑 → (((𝑄 ∨ 𝑅) ∨ 𝑃) ∈ 𝑂 ∧ ((𝑇 ∨ 𝑈) ∨ 𝑆) ∈ 𝑂)) | 
| 28 |  | simp312 1322 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑄 ∨ 𝑅)) | 
| 29 | 1, 28 | sylbi 217 | . . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑄 ∨ 𝑅)) | 
| 30 |  | simp313 1323 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) | 
| 31 | 1, 30 | sylbi 217 | . . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) | 
| 32 | 1 | dalem-clpjq 39639 | . . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) | 
| 33 | 29, 31, 32 | 3jca 1129 | . . 3
⊢ (𝜑 → (¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃) ∧ ¬ 𝐶 ≤ (𝑃 ∨ 𝑄))) | 
| 34 |  | simp322 1325 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑇 ∨ 𝑈)) | 
| 35 | 1, 34 | sylbi 217 | . . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑇 ∨ 𝑈)) | 
| 36 |  | simp323 1326 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) | 
| 37 | 1, 36 | sylbi 217 | . . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) | 
| 38 |  | simp321 1324 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) | 
| 39 | 1, 38 | sylbi 217 | . . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) | 
| 40 | 35, 37, 39 | 3jca 1129 | . . 3
⊢ (𝜑 → (¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆) ∧ ¬ 𝐶 ≤ (𝑆 ∨ 𝑇))) | 
| 41 | 1 | dalemclqjt 39637 | . . . 4
⊢ (𝜑 → 𝐶 ≤ (𝑄 ∨ 𝑇)) | 
| 42 | 1 | dalemclrju 39638 | . . . 4
⊢ (𝜑 → 𝐶 ≤ (𝑅 ∨ 𝑈)) | 
| 43 | 1 | dalemclpjs 39636 | . . . 4
⊢ (𝜑 → 𝐶 ≤ (𝑃 ∨ 𝑆)) | 
| 44 | 41, 42, 43 | 3jca 1129 | . . 3
⊢ (𝜑 → (𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈) ∧ 𝐶 ≤ (𝑃 ∨ 𝑆))) | 
| 45 | 33, 40, 44 | 3jca 1129 | . 2
⊢ (𝜑 → ((¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃) ∧ ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆) ∧ ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) ∧ (𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈) ∧ 𝐶 ≤ (𝑃 ∨ 𝑆)))) | 
| 46 | 14, 27, 45 | 3jca 1129 | 1
⊢ (𝜑 → (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ (𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ (((𝑄 ∨ 𝑅) ∨ 𝑃) ∈ 𝑂 ∧ ((𝑇 ∨ 𝑈) ∨ 𝑆) ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃) ∧ ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆) ∧ ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) ∧ (𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈) ∧ 𝐶 ≤ (𝑃 ∨ 𝑆))))) |