Metamath Proof Explorer

Theorem rehaus

Description: The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007)

Ref Expression
Assertion rehaus 
|- ( topGen ` ran (,) ) e. Haus

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
2 1 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
3 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
4 1 3 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
5 4 methaus 
 |-  ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) -> ( topGen ` ran (,) ) e. Haus )
6 2 5 ax-mp 
 |-  ( topGen ` ran (,) ) e. Haus