Theorem cnfldtps

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

	Ref	Expression
Assertion	cnfldtps	⊢ ℂfld ∈ TopSp

Proof

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