Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Thierry Arnoux, 3-Jul-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | tgioo3.1 | ⊢ 𝐽 = ( TopOpen ‘ ℝfld ) | |
| Assertion | tgioo3 | ⊢ ( topGen ‘ ran (,) ) = 𝐽 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tgioo3.1 | ⊢ 𝐽 = ( TopOpen ‘ ℝfld ) | |
| 2 | eqid | ⊢ ( ℂfld ↾s ℝ ) = ( ℂfld ↾s ℝ ) | |
| 3 | eqid | ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) | |
| 4 | 2 3 | resstopn | ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( TopOpen ‘ ( ℂfld ↾s ℝ ) ) |
| 5 | tgioo4 | ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) | |
| 6 | df-refld | ⊢ ℝfld = ( ℂfld ↾s ℝ ) | |
| 7 | 6 | fveq2i | ⊢ ( TopOpen ‘ ℝfld ) = ( TopOpen ‘ ( ℂfld ↾s ℝ ) ) |
| 8 | 1 7 | eqtri | ⊢ 𝐽 = ( TopOpen ‘ ( ℂfld ↾s ℝ ) ) |
| 9 | 4 5 8 | 3eqtr4i | ⊢ ( topGen ‘ ran (,) ) = 𝐽 |