Theorem cnfldxms

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

	Ref	Expression
Assertion	cnfldxms	⊢ ℂfld ∈ ∞MetSp

Proof

Step	Hyp	Ref	Expression
1		cnfldms	⊢ ℂfld ∈ MetSp
2		msxms	⊢ ( ℂfld ∈ MetSp → ℂfld ∈ ∞MetSp )
3	1 2	ax-mp	⊢ ℂfld ∈ ∞MetSp