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 ` ( RR*s |`s ( 0 [,] +oo ) ) ) e. Haus

Proof

Step	Hyp	Ref	Expression
1		xrge0topn	|- ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
2		xrhaus	|- ( ordTop ` <_ ) e. Haus
3		ovex	|- ( 0 [,] +oo ) e. _V
4		resthaus	|- ( ( ( ordTop ` <_ ) e. Haus /\ ( 0 [,] +oo ) e. _V ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus )
5	2 3 4	mp2an	|- ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus
6	1 5	eqeltri	|- ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) e. Haus