Metamath Proof Explorer


Theorem xrge0haus

Description: The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017)

Ref Expression
Assertion xrge0haus TopOpen𝑠*𝑠0+∞Haus

Proof

Step Hyp Ref Expression
1 xrge0topn TopOpen𝑠*𝑠0+∞=ordTop𝑡0+∞
2 xrhaus ordTopHaus
3 ovex 0+∞V
4 resthaus ordTopHaus0+∞VordTop𝑡0+∞Haus
5 2 3 4 mp2an ordTop𝑡0+∞Haus
6 1 5 eqeltri TopOpen𝑠*𝑠0+∞Haus