Theorem rehaus

Description: The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007)

	Ref	Expression
Assertion	rehaus	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Haus}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
2	1	rexmet	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{\infty Met}\left(ℝ\right)$$
3		eqid	$$⊢\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
4	1 3	tgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
5	4	methaus	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{\infty Met}\left(ℝ\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Haus}$$
6	2 5	ax-mp	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Haus}$$