Theorem cnfldtopn

Description: The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypothesis	cnfldtopn.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnfldtopn	$$⊢J=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnfldtopn.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		cnxmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$$
3		eqid	$$⊢\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$
4	3	mopntopon	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\to \mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\in \mathrm{TopOn}\left(ℂ\right)$$
5		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
6		cnfldtset	$$⊢\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{TopSet}\left({ℂ}_{\mathrm{fld}}\right)$$
7	5 6	topontopn	$$⊢\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\in \mathrm{TopOn}\left(ℂ\right)\to \mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
8	2 4 7	mp2b	$$⊢\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
9	1 8	eqtr4i	$$⊢J=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$