Step | Hyp | Ref
| Expression |
1 | | topdlat.i |
. . . 4
⊢ 𝐼 = (toInc‘𝐽) |
2 | 1 | topclat 46284 |
. . 3
⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat) |
3 | | clatl 18226 |
. . 3
⊢ (𝐼 ∈ CLat → 𝐼 ∈ Lat) |
4 | 2, 3 | syl 17 |
. 2
⊢ (𝐽 ∈ Top → 𝐼 ∈ Lat) |
5 | | simpl 483 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → 𝐽 ∈ Top) |
6 | | simpr2 1194 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → 𝑦 ∈ (Base‘𝐼)) |
7 | 1 | ipobas 18249 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → 𝐽 = (Base‘𝐼)) |
8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → 𝐽 = (Base‘𝐼)) |
9 | 6, 8 | eleqtrrd 2842 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → 𝑦 ∈ 𝐽) |
10 | | simpr3 1195 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → 𝑧 ∈ (Base‘𝐼)) |
11 | 10, 8 | eleqtrrd 2842 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → 𝑧 ∈ 𝐽) |
12 | | eqid 2738 |
. . . . . 6
⊢
(join‘𝐼) =
(join‘𝐼) |
13 | 1, 5, 9, 11, 12 | toplatjoin 46288 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑦(join‘𝐼)𝑧) = (𝑦 ∪ 𝑧)) |
14 | 13 | oveq2d 7291 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥(meet‘𝐼)(𝑦(join‘𝐼)𝑧)) = (𝑥(meet‘𝐼)(𝑦 ∪ 𝑧))) |
15 | | simpr1 1193 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → 𝑥 ∈ (Base‘𝐼)) |
16 | 15, 8 | eleqtrrd 2842 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → 𝑥 ∈ 𝐽) |
17 | | unopn 22052 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) → (𝑦 ∪ 𝑧) ∈ 𝐽) |
18 | 5, 9, 11, 17 | syl3anc 1370 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑦 ∪ 𝑧) ∈ 𝐽) |
19 | | eqid 2738 |
. . . . 5
⊢
(meet‘𝐼) =
(meet‘𝐼) |
20 | 1, 5, 16, 18, 19 | toplatmeet 46289 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥(meet‘𝐼)(𝑦 ∪ 𝑧)) = (𝑥 ∩ (𝑦 ∪ 𝑧))) |
21 | | inopn 22048 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∩ 𝑦) ∈ 𝐽) |
22 | 5, 16, 9, 21 | syl3anc 1370 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥 ∩ 𝑦) ∈ 𝐽) |
23 | | inopn 22048 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) → (𝑥 ∩ 𝑧) ∈ 𝐽) |
24 | 5, 16, 11, 23 | syl3anc 1370 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥 ∩ 𝑧) ∈ 𝐽) |
25 | 1, 5, 22, 24, 12 | toplatjoin 46288 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → ((𝑥 ∩ 𝑦)(join‘𝐼)(𝑥 ∩ 𝑧)) = ((𝑥 ∩ 𝑦) ∪ (𝑥 ∩ 𝑧))) |
26 | 1, 5, 16, 9, 19 | toplatmeet 46289 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥(meet‘𝐼)𝑦) = (𝑥 ∩ 𝑦)) |
27 | 1, 5, 16, 11, 19 | toplatmeet 46289 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥(meet‘𝐼)𝑧) = (𝑥 ∩ 𝑧)) |
28 | 26, 27 | oveq12d 7293 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → ((𝑥(meet‘𝐼)𝑦)(join‘𝐼)(𝑥(meet‘𝐼)𝑧)) = ((𝑥 ∩ 𝑦)(join‘𝐼)(𝑥 ∩ 𝑧))) |
29 | | indi 4207 |
. . . . . 6
⊢ (𝑥 ∩ (𝑦 ∪ 𝑧)) = ((𝑥 ∩ 𝑦) ∪ (𝑥 ∩ 𝑧)) |
30 | 29 | a1i 11 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥 ∩ (𝑦 ∪ 𝑧)) = ((𝑥 ∩ 𝑦) ∪ (𝑥 ∩ 𝑧))) |
31 | 25, 28, 30 | 3eqtr4rd 2789 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥 ∩ (𝑦 ∪ 𝑧)) = ((𝑥(meet‘𝐼)𝑦)(join‘𝐼)(𝑥(meet‘𝐼)𝑧))) |
32 | 14, 20, 31 | 3eqtrd 2782 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝑥 ∈ (Base‘𝐼) ∧ 𝑦 ∈ (Base‘𝐼) ∧ 𝑧 ∈ (Base‘𝐼))) → (𝑥(meet‘𝐼)(𝑦(join‘𝐼)𝑧)) = ((𝑥(meet‘𝐼)𝑦)(join‘𝐼)(𝑥(meet‘𝐼)𝑧))) |
33 | 32 | ralrimivvva 3127 |
. 2
⊢ (𝐽 ∈ Top → ∀𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)∀𝑧 ∈ (Base‘𝐼)(𝑥(meet‘𝐼)(𝑦(join‘𝐼)𝑧)) = ((𝑥(meet‘𝐼)𝑦)(join‘𝐼)(𝑥(meet‘𝐼)𝑧))) |
34 | | eqid 2738 |
. . 3
⊢
(Base‘𝐼) =
(Base‘𝐼) |
35 | 34, 12, 19 | isdlat 18240 |
. 2
⊢ (𝐼 ∈ DLat ↔ (𝐼 ∈ Lat ∧ ∀𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)∀𝑧 ∈ (Base‘𝐼)(𝑥(meet‘𝐼)(𝑦(join‘𝐼)𝑧)) = ((𝑥(meet‘𝐼)𝑦)(join‘𝐼)(𝑥(meet‘𝐼)𝑧)))) |
36 | 4, 33, 35 | sylanbrc 583 |
1
⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat) |