Metamath Proof Explorer

Theorem retopbas

Description: A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007) (Proof shortened by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion retopbas 
|- ran (,) e. TopBases

Proof

Step Hyp Ref Expression
1 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
2 1 fdmi 
 |-  dom (,) = ( RR* X. RR* )
3 2 imaeq2i 
 |-  ( (,) " dom (,) ) = ( (,) " ( RR* X. RR* ) )
4 imadmrn 
 |-  ( (,) " dom (,) ) = ran (,)
5 3 4 eqtr3i 
 |-  ( (,) " ( RR* X. RR* ) ) = ran (,)
6 ssid 
 |-  RR* C_ RR*
7 6 qtopbaslem 
 |-  ( (,) " ( RR* X. RR* ) ) e. TopBases
8 5 7 eqeltrri 
 |-  ran (,) e. TopBases