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 ⊢ ordTop ⁡ ≤ ∈ Haus
3 ovex ⊢ 0 +∞ ∈ V
4 resthaus ⊢ ordTop ⁡ ≤ ∈ Haus ∧ 0 +∞ ∈ V → ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ∈ Haus
5 2 3 4 mp2an ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ∈ Haus
6 1 5 eqeltri ⊢ TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Haus