Description: The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnopn | |- CC e. ( TopOpen ` CCfld ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unicntop | |- CC = U. ( TopOpen ` CCfld ) |
|
| 2 | eqid | |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
|
| 3 | 2 | cnfldtop | |- ( TopOpen ` CCfld ) e. Top |
| 4 | ssid | |- ( TopOpen ` CCfld ) C_ ( TopOpen ` CCfld ) |
|
| 5 | uniopn | |- ( ( ( TopOpen ` CCfld ) e. Top /\ ( TopOpen ` CCfld ) C_ ( TopOpen ` CCfld ) ) -> U. ( TopOpen ` CCfld ) e. ( TopOpen ` CCfld ) ) |
|
| 6 | 3 4 5 | mp2an | |- U. ( TopOpen ` CCfld ) e. ( TopOpen ` CCfld ) |
| 7 | 1 6 | eqeltri | |- CC e. ( TopOpen ` CCfld ) |