Metamath Proof Explorer

Theorem retopon

Description: The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Assertion retopon 
|- ( topGen ` ran (,) ) e. ( TopOn ` RR )

Proof

Step Hyp Ref Expression
1 retop 
 |-  ( topGen ` ran (,) ) e. Top
2 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
3 2 toptopon 
 |-  ( ( topGen ` ran (,) ) e. Top <-> ( topGen ` ran (,) ) e. ( TopOn ` RR ) )
4 1 3 mpbi 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )