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 ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ∈ Haus

Proof

Step	Hyp	Ref	Expression
1		xrge0topn	⊢ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
2		xrhaus	⊢ ( ordTop ‘ ≤ ) ∈ Haus
3		ovex	⊢ ( 0 [,] +∞ ) ∈ V
4		resthaus	⊢ ( ( ( ordTop ‘ ≤ ) ∈ Haus ∧ ( 0 [,] +∞ ) ∈ V ) → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus )
5	2 3 4	mp2an	⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus
6	1 5	eqeltri	⊢ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ∈ Haus