Proof of Theorem ressusp
Step | Hyp | Ref
| Expression |
1 | | ressuss 23160 |
. . . . 5
⊢ (𝐴 ∈ 𝐽 → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴))) |
2 | 1 | 3ad2ant3 1137 |
. . . 4
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴))) |
3 | | simp1 1138 |
. . . . . . 7
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝑊 ∈ UnifSp) |
4 | | ressusp.1 |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑊) |
5 | | eqid 2737 |
. . . . . . . 8
⊢
(UnifSt‘𝑊) =
(UnifSt‘𝑊) |
6 | | ressusp.2 |
. . . . . . . 8
⊢ 𝐽 = (TopOpen‘𝑊) |
7 | 4, 5, 6 | isusp 23159 |
. . . . . . 7
⊢ (𝑊 ∈ UnifSp ↔
((UnifSt‘𝑊) ∈
(UnifOn‘𝐵) ∧
𝐽 =
(unifTop‘(UnifSt‘𝑊)))) |
8 | 3, 7 | sylib 221 |
. . . . . 6
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → ((UnifSt‘𝑊) ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑊)))) |
9 | 8 | simpld 498 |
. . . . 5
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifSt‘𝑊) ∈ (UnifOn‘𝐵)) |
10 | | simp2 1139 |
. . . . . . 7
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝑊 ∈ TopSp) |
11 | 4, 6 | istps 21831 |
. . . . . . 7
⊢ (𝑊 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐵)) |
12 | 10, 11 | sylib 221 |
. . . . . 6
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐽 ∈ (TopOn‘𝐵)) |
13 | | simp3 1140 |
. . . . . 6
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐴 ∈ 𝐽) |
14 | | toponss 21824 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝐵) |
15 | 12, 13, 14 | syl2anc 587 |
. . . . 5
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝐵) |
16 | | trust 23127 |
. . . . 5
⊢
(((UnifSt‘𝑊)
∈ (UnifOn‘𝐵)
∧ 𝐴 ⊆ 𝐵) → ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴)) |
17 | 9, 15, 16 | syl2anc 587 |
. . . 4
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴)) |
18 | 2, 17 | eqeltrd 2838 |
. . 3
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifSt‘(𝑊 ↾s 𝐴)) ∈ (UnifOn‘𝐴)) |
19 | | eqid 2737 |
. . . . . 6
⊢ (𝑊 ↾s 𝐴) = (𝑊 ↾s 𝐴) |
20 | 19, 4 | ressbas2 16791 |
. . . . 5
⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘(𝑊 ↾s 𝐴))) |
21 | 15, 20 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐴 = (Base‘(𝑊 ↾s 𝐴))) |
22 | 21 | fveq2d 6721 |
. . 3
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifOn‘𝐴) = (UnifOn‘(Base‘(𝑊 ↾s 𝐴)))) |
23 | 18, 22 | eleqtrd 2840 |
. 2
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (UnifSt‘(𝑊 ↾s 𝐴)) ∈ (UnifOn‘(Base‘(𝑊 ↾s 𝐴)))) |
24 | 8 | simprd 499 |
. . . . 5
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐽 = (unifTop‘(UnifSt‘𝑊))) |
25 | 13, 24 | eleqtrd 2840 |
. . . 4
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → 𝐴 ∈ (unifTop‘(UnifSt‘𝑊))) |
26 | | restutopopn 23136 |
. . . 4
⊢
(((UnifSt‘𝑊)
∈ (UnifOn‘𝐵)
∧ 𝐴 ∈
(unifTop‘(UnifSt‘𝑊))) →
((unifTop‘(UnifSt‘𝑊)) ↾t 𝐴) = (unifTop‘((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)))) |
27 | 9, 25, 26 | syl2anc 587 |
. . 3
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → ((unifTop‘(UnifSt‘𝑊)) ↾t 𝐴) =
(unifTop‘((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)))) |
28 | 24 | oveq1d 7228 |
. . 3
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝐽 ↾t 𝐴) = ((unifTop‘(UnifSt‘𝑊)) ↾t 𝐴)) |
29 | 2 | fveq2d 6721 |
. . 3
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (unifTop‘(UnifSt‘(𝑊 ↾s 𝐴))) =
(unifTop‘((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)))) |
30 | 27, 28, 29 | 3eqtr4d 2787 |
. 2
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝐽 ↾t 𝐴) = (unifTop‘(UnifSt‘(𝑊 ↾s 𝐴)))) |
31 | | eqid 2737 |
. . 3
⊢
(Base‘(𝑊
↾s 𝐴)) =
(Base‘(𝑊
↾s 𝐴)) |
32 | | eqid 2737 |
. . 3
⊢
(UnifSt‘(𝑊
↾s 𝐴)) =
(UnifSt‘(𝑊
↾s 𝐴)) |
33 | 19, 6 | resstopn 22083 |
. . 3
⊢ (𝐽 ↾t 𝐴) = (TopOpen‘(𝑊 ↾s 𝐴)) |
34 | 31, 32, 33 | isusp 23159 |
. 2
⊢ ((𝑊 ↾s 𝐴) ∈ UnifSp ↔
((UnifSt‘(𝑊
↾s 𝐴))
∈ (UnifOn‘(Base‘(𝑊 ↾s 𝐴))) ∧ (𝐽 ↾t 𝐴) = (unifTop‘(UnifSt‘(𝑊 ↾s 𝐴))))) |
35 | 23, 30, 34 | sylanbrc 586 |
1
⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝑊 ↾s 𝐴) ∈ UnifSp) |