Metamath Proof Explorer

Theorem xrhaus

Description: The topology of the extended reals is Hausdorff. (Contributed by Thierry Arnoux, 24-Mar-2017)

Ref Expression
Assertion xrhaus 
|- ( ordTop ` <_ ) e. Haus

Proof

Step Hyp Ref Expression
1 letsr 
 |-  <_ e. TosetRel
2 ordthaus 
 |-  ( <_ e. TosetRel -> ( ordTop ` <_ ) e. Haus )
3 1 2 ax-mp 
 |-  ( ordTop ` <_ ) e. Haus