Metamath Proof Explorer

Theorem reopn

Description: The reals are open with respect to the standard topology. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 retop 
 |-  ( topGen ` ran (,) ) e. Top
2 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
3 2 topopn 
 |-  ( ( topGen ` ran (,) ) e. Top -> RR e. ( topGen ` ran (,) ) )
4 1 3 ax-mp 
 |-  RR e. ( topGen ` ran (,) )