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=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnfldtopon	$$⊢J\in \mathrm{TopOn}\left(ℂ\right)$$

Proof

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