Theorem cnfldhaus

Description: The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015)

	Ref	Expression
Hypothesis	cnfldtopn.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnfldhaus	$$⊢J\in \mathrm{Haus}$$

Proof

Step	Hyp	Ref	Expression
1		cnfldtopn.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		cnxmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$$
3	1	cnfldtopn	$$⊢J=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$
4	3	methaus	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\to J\in \mathrm{Haus}$$
5	2 4	ax-mp	$$⊢J\in \mathrm{Haus}$$