Metamath Proof Explorer

Theorem iooretop

Description: Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007)

Ref Expression
Assertion iooretop 
|- ( A (,) B ) e. ( topGen ` ran (,) )

Proof

Step Hyp Ref Expression
1 retopbas 
 |-  ran (,) e. TopBases
2 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
3 1 2 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
4 ioorebas 
 |-  ( A (,) B ) e. ran (,)
5 3 4 sselii 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )