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