Theorem cnfldtopn

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

	Ref	Expression
Hypothesis	cnfldtopn.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	cnfldtopn	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )

Proof

Step	Hyp	Ref	Expression
1		cnfldtopn.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
3		eqid	⊢ ( MetOpen ‘ ( abs ∘ − ) ) = ( MetOpen ‘ ( abs ∘ − ) )
4	3	mopntopon	⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → ( MetOpen ‘ ( abs ∘ − ) ) ∈ ( TopOn ‘ ℂ ) )
5		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
6		cnfldtset	⊢ ( MetOpen ‘ ( abs ∘ − ) ) = ( TopSet ‘ ℂfld )
7	5 6	topontopn	⊢ ( ( MetOpen ‘ ( abs ∘ − ) ) ∈ ( TopOn ‘ ℂ ) → ( MetOpen ‘ ( abs ∘ − ) ) = ( TopOpen ‘ ℂfld ) )
8	2 4 7	mp2b	⊢ ( MetOpen ‘ ( abs ∘ − ) ) = ( TopOpen ‘ ℂfld )
9	1 8	eqtr4i	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )