Metamath Proof Explorer

Theorem tgioo2

Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypothesis tgioo2.1 
|- J = ( TopOpen ` CCfld )
Assertion tgioo2 
|- ( topGen ` ran (,) ) = ( J |`t RR )

Proof

Step Hyp Ref Expression
1 tgioo2.1 
 |-  J = ( TopOpen ` CCfld )
2 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
3 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
4 ax-resscn 
 |-  RR C_ CC
5 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
6 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
7 2 5 6 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ RR C_ CC ) -> ( J |`t RR ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) )
8 3 4 7 mp2an 
 |-  ( J |`t RR ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
9 2 8 tgioo 
 |-  ( topGen ` ran (,) ) = ( J |`t RR )