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
|- CC = U. ( TopOpen ` CCfld )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 1 cnfldtopon
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
3 2 toponunii
 |-  CC = U. ( TopOpen ` CCfld )