# Metamath Proof Explorer

## 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)$