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