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
|- J = ( TopOpen ` RRfld )
Assertion tgioo3
|- ( topGen ` ran (,) ) = J

Proof

Step Hyp Ref Expression
1 tgioo3.1
 |-  J = ( TopOpen ` RRfld )
2 eqid
 |-  ( CCfld |`s RR ) = ( CCfld |`s RR )
3 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 2 3 resstopn
 |-  ( ( TopOpen ` CCfld ) |`t RR ) = ( TopOpen ` ( CCfld |`s RR ) )
5 3 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
6 df-refld
 |-  RRfld = ( CCfld |`s RR )
7 6 fveq2i
 |-  ( TopOpen ` RRfld ) = ( TopOpen ` ( CCfld |`s RR ) )
8 1 7 eqtri
 |-  J = ( TopOpen ` ( CCfld |`s RR ) )
9 4 5 8 3eqtr4i
 |-  ( topGen ` ran (,) ) = J