This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ ≤ ) ∈ Haus

Proof

Step Hyp Ref Expression
1 letsr ⊢ ≤ ∈ TosetRel
2 ordthaus ⊢ ( ≤ ∈ TosetRel → ( ordTop ‘ ≤ ) ∈ Haus )
3 1 2 ax-mp ⊢ ( ordTop ‘ ≤ ) ∈ Haus