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 ` CCfld )
Assertion	cnfldtopon	|- J e. ( TopOn ` CC )

Proof

Step	Hyp	Ref	Expression
1		cnfldtopn.1	|- J = ( TopOpen ` CCfld )
2		cnfldtps	|- CCfld e. TopSp
3		cnfldbas	|- CC = ( Base ` CCfld )
4	3 1	istps	|- ( CCfld e. TopSp <-> J e. ( TopOn ` CC ) )
5	2 4	mpbi	|- J e. ( TopOn ` CC )