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 =TopOpenfld

Proof

Step Hyp Ref Expression
1 eqid TopOpenfld=TopOpenfld
2 1 cnfldtopon TopOpenfldTopOn
3 2 toponunii =TopOpenfld