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

Metamath Proof Explorer

Theorem cnfldtopon

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	cnfldtopon	$⊢ J \in TopOn (ℂ)$

Step	Hyp	Ref	Expression
1		cnfldtopn.1	$⊢ J = TopOpen (ℂ_{fld})$
2		cnfldtps	$⊢ ℂ_{fld} \in TopSp$
3		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
4	3 1	istps	$⊢ ℂ_{fld} \in TopSp \leftrightarrow J \in TopOn (ℂ)$
5	2 4	mpbi	$⊢ J \in TopOn (ℂ)$