Metamath Proof Explorer

Theorem tgioo4

Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Assertion tgioo4 
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 1 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )