Proof of Theorem dalem5
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. 2
⊢
(Base‘𝐾) =
(Base‘𝐾) |
2 | | dalemc.l |
. 2
⊢ ≤ =
(le‘𝐾) |
3 | | dalema.ph |
. . 3
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
4 | 3 | dalemkelat 37638 |
. 2
⊢ (𝜑 → 𝐾 ∈ Lat) |
5 | | dalemc.a |
. . 3
⊢ 𝐴 = (Atoms‘𝐾) |
6 | 3, 5 | dalemueb 37658 |
. 2
⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾)) |
7 | 3 | dalemkehl 37637 |
. . 3
⊢ (𝜑 → 𝐾 ∈ HL) |
8 | 3 | dalemrea 37642 |
. . 3
⊢ (𝜑 → 𝑅 ∈ 𝐴) |
9 | | dalemc.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
10 | | dalem5.o |
. . . 4
⊢ 𝑂 = (LPlanes‘𝐾) |
11 | | dalem5.y |
. . . 4
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) |
12 | 3, 2, 9, 5, 10, 11 | dalemcea 37674 |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
13 | 1, 9, 5 | hlatjcl 37381 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝑅 ∨ 𝐶) ∈ (Base‘𝐾)) |
14 | 7, 8, 12, 13 | syl3anc 1370 |
. 2
⊢ (𝜑 → (𝑅 ∨ 𝐶) ∈ (Base‘𝐾)) |
15 | | dalem5.w |
. . 3
⊢ 𝑊 = (𝑌 ∨ 𝐶) |
16 | 3, 10 | dalemyeb 37663 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾)) |
17 | 3, 5 | dalemceb 37652 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾)) |
18 | 1, 9 | latjcl 18157 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾)) → (𝑌 ∨ 𝐶) ∈ (Base‘𝐾)) |
19 | 4, 16, 17, 18 | syl3anc 1370 |
. . 3
⊢ (𝜑 → (𝑌 ∨ 𝐶) ∈ (Base‘𝐾)) |
20 | 15, 19 | eqeltrid 2843 |
. 2
⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾)) |
21 | 3 | dalemclrju 37650 |
. . 3
⊢ (𝜑 → 𝐶 ≤ (𝑅 ∨ 𝑈)) |
22 | 3 | dalemuea 37645 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝐴) |
23 | 3 | dalempea 37640 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
24 | | simp313 1321 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) |
25 | 3, 24 | sylbi 216 |
. . . . 5
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) |
26 | 2, 9, 5 | atnlej1 37393 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) → 𝐶 ≠ 𝑅) |
27 | 7, 12, 8, 23, 25, 26 | syl131anc 1382 |
. . . 4
⊢ (𝜑 → 𝐶 ≠ 𝑅) |
28 | 2, 9, 5 | hlatexch1 37409 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝐶 ≠ 𝑅) → (𝐶 ≤ (𝑅 ∨ 𝑈) → 𝑈 ≤ (𝑅 ∨ 𝐶))) |
29 | 7, 12, 22, 8, 27, 28 | syl131anc 1382 |
. . 3
⊢ (𝜑 → (𝐶 ≤ (𝑅 ∨ 𝑈) → 𝑈 ≤ (𝑅 ∨ 𝐶))) |
30 | 21, 29 | mpd 15 |
. 2
⊢ (𝜑 → 𝑈 ≤ (𝑅 ∨ 𝐶)) |
31 | 3, 9, 5 | dalempjqeb 37659 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
32 | 3, 5 | dalemreb 37655 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ (Base‘𝐾)) |
33 | 1, 2, 9 | latlej2 18167 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
34 | 4, 31, 32, 33 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
35 | 34, 11 | breqtrrdi 5116 |
. . . 4
⊢ (𝜑 → 𝑅 ≤ 𝑌) |
36 | 1, 2, 9 | latjlej1 18171 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾))) → (𝑅 ≤ 𝑌 → (𝑅 ∨ 𝐶) ≤ (𝑌 ∨ 𝐶))) |
37 | 4, 32, 16, 17, 36 | syl13anc 1371 |
. . . 4
⊢ (𝜑 → (𝑅 ≤ 𝑌 → (𝑅 ∨ 𝐶) ≤ (𝑌 ∨ 𝐶))) |
38 | 35, 37 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑅 ∨ 𝐶) ≤ (𝑌 ∨ 𝐶)) |
39 | 38, 15 | breqtrrdi 5116 |
. 2
⊢ (𝜑 → (𝑅 ∨ 𝐶) ≤ 𝑊) |
40 | 1, 2, 4, 6, 14, 20, 30, 39 | lattrd 18164 |
1
⊢ (𝜑 → 𝑈 ≤ 𝑊) |