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