Metamath Proof Explorer


Theorem unicntop

Description: The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion unicntop ℂ = ( TopOpen ‘ ℂfld )

Proof

Step Hyp Ref Expression
1 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2 1 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
3 2 toponunii ℂ = ( TopOpen ‘ ℂfld )