Theorem cnfldxms

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

	Ref	Expression
Assertion	cnfldxms	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{\infty MetSp}$$

Proof

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