Metamath Proof Explorer


Theorem tgioo3

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 (,) ) = 𝐽

Proof

Step Hyp Ref Expression
1 tgioo3.1 𝐽 = ( TopOpen ‘ ℝfld )
2 eqid ( ℂflds ℝ ) = ( ℂflds ℝ )
3 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4 2 3 resstopn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( TopOpen ‘ ( ℂflds ℝ ) )
5 3 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
6 df-refld fld = ( ℂflds ℝ )
7 6 fveq2i ( TopOpen ‘ ℝfld ) = ( TopOpen ‘ ( ℂflds ℝ ) )
8 1 7 eqtri 𝐽 = ( TopOpen ‘ ( ℂflds ℝ ) )
9 4 5 8 3eqtr4i ( topGen ‘ ran (,) ) = 𝐽