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