This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfldtop

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

		Ref	Expression
	Hypothesis	cnfldtopn.1	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	cnfldtop	$⊢ J \in Top$

Step	Hyp	Ref	Expression
1		cnfldtopn.1	$⊢ J = TopOpen (ℂ_{fld})$
2	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
3	2	topontopi	$⊢ J \in Top$