Theorem cnfldtps

Description: The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Assertion	cnfldtps	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		cnfldms	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}$$
2		mstps	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}\to {ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$$
3	1 2	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$$