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