Metamath Proof Explorer

Theorem uniretop

Description: The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007)

Ref Expression
Assertion uniretop 
|- RR = U. ( topGen ` ran (,) )

Proof

Step Hyp Ref Expression
1 unirnioo 
 |-  RR = U. ran (,)
2 retopbas 
 |-  ran (,) e. TopBases
3 unitg 
 |-  ( ran (,) e. TopBases -> U. ( topGen ` ran (,) ) = U. ran (,) )
4 2 3 ax-mp 
 |-  U. ( topGen ` ran (,) ) = U. ran (,)
5 1 4 eqtr4i 
 |-  RR = U. ( topGen ` ran (,) )