Proof of Theorem dalemrot
Step | Hyp | Ref
| Expression |
1 | | dalema.ph |
. . . . 5
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
2 | 1 | dalemkehl 37249 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ HL) |
3 | | dalemc.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
4 | 1, 3 | dalemceb 37264 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾)) |
5 | 2, 4 | jca 515 |
. . 3
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾))) |
6 | 1 | dalemqea 37253 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
7 | 1 | dalemrea 37254 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝐴) |
8 | 1 | dalempea 37252 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
9 | 6, 7, 8 | 3jca 1129 |
. . 3
⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴)) |
10 | 1 | dalemtea 37256 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
11 | 1 | dalemuea 37257 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝐴) |
12 | 1 | dalemsea 37255 |
. . . 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 37274 |
. . . 4
⊢ (𝜑 → ((𝑄 ∨ 𝑅) ∨ 𝑃) = ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
17 | | dalemrot.y |
. . . . 5
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) |
18 | 1 | dalemyeo 37258 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑂) |
19 | 17, 18 | eqeltrrid 2838 |
. . . 4
⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂) |
20 | 16, 19 | eqeltrd 2833 |
. . 3
⊢ (𝜑 → ((𝑄 ∨ 𝑅) ∨ 𝑃) ∈ 𝑂) |
21 | 15, 3 | hlatjrot 36999 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑇 ∨ 𝑈) ∨ 𝑆) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) |
22 | 2, 10, 11, 12, 21 | syl13anc 1373 |
. . . 4
⊢ (𝜑 → ((𝑇 ∨ 𝑈) ∨ 𝑆) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) |
23 | | dalemrot.z |
. . . . 5
⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) |
24 | 1 | dalemzeo 37259 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑂) |
25 | 23, 24 | eqeltrrid 2838 |
. . . 4
⊢ (𝜑 → ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂) |
26 | 22, 25 | eqeltrd 2833 |
. . 3
⊢ (𝜑 → ((𝑇 ∨ 𝑈) ∨ 𝑆) ∈ 𝑂) |
27 | 20, 26 | jca 515 |
. 2
⊢ (𝜑 → (((𝑄 ∨ 𝑅) ∨ 𝑃) ∈ 𝑂 ∧ ((𝑇 ∨ 𝑈) ∨ 𝑆) ∈ 𝑂)) |
28 | | simp312 1322 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑄 ∨ 𝑅)) |
29 | 1, 28 | sylbi 220 |
. . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑄 ∨ 𝑅)) |
30 | | simp313 1323 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) |
31 | 1, 30 | sylbi 220 |
. . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) |
32 | 1 | dalem-clpjq 37263 |
. . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) |
33 | 29, 31, 32 | 3jca 1129 |
. . 3
⊢ (𝜑 → (¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃) ∧ ¬ 𝐶 ≤ (𝑃 ∨ 𝑄))) |
34 | | simp322 1325 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑇 ∨ 𝑈)) |
35 | 1, 34 | sylbi 220 |
. . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑇 ∨ 𝑈)) |
36 | | simp323 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) |
37 | 1, 36 | sylbi 220 |
. . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) |
38 | | simp321 1324 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) |
39 | 1, 38 | sylbi 220 |
. . . 4
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) |
40 | 35, 37, 39 | 3jca 1129 |
. . 3
⊢ (𝜑 → (¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆) ∧ ¬ 𝐶 ≤ (𝑆 ∨ 𝑇))) |
41 | 1 | dalemclqjt 37261 |
. . . 4
⊢ (𝜑 → 𝐶 ≤ (𝑄 ∨ 𝑇)) |
42 | 1 | dalemclrju 37262 |
. . . 4
⊢ (𝜑 → 𝐶 ≤ (𝑅 ∨ 𝑈)) |
43 | 1 | dalemclpjs 37260 |
. . . 4
⊢ (𝜑 → 𝐶 ≤ (𝑃 ∨ 𝑆)) |
44 | 41, 42, 43 | 3jca 1129 |
. . 3
⊢ (𝜑 → (𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈) ∧ 𝐶 ≤ (𝑃 ∨ 𝑆))) |
45 | 33, 40, 44 | 3jca 1129 |
. 2
⊢ (𝜑 → ((¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃) ∧ ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆) ∧ ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) ∧ (𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈) ∧ 𝐶 ≤ (𝑃 ∨ 𝑆)))) |
46 | 14, 27, 45 | 3jca 1129 |
1
⊢ (𝜑 → (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ (𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ (((𝑄 ∨ 𝑅) ∨ 𝑃) ∈ 𝑂 ∧ ((𝑇 ∨ 𝑈) ∨ 𝑆) ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃) ∧ ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆) ∧ ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) ∧ (𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈) ∧ 𝐶 ≤ (𝑃 ∨ 𝑆))))) |