Metamath Proof Explorer

Theorem retop

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

Ref Expression
Assertion retop 
|- ( topGen ` ran (,) ) e. Top

Proof

Step Hyp Ref Expression
1 retopbas 
 |-  ran (,) e. TopBases
2 tgcl 
 |-  ( ran (,) e. TopBases -> ( topGen ` ran (,) ) e. Top )
3 1 2 ax-mp 
 |-  ( topGen ` ran (,) ) e. Top