Description: The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | recld2.1 | |- J = ( TopOpen ` CCfld ) |
|
| Assertion | cnperf | |- J e. Perf |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | recld2.1 | |- J = ( TopOpen ` CCfld ) |
|
| 2 | 1 | cnfldtopon | |- J e. ( TopOn ` CC ) |
| 3 | 2 | toponunii | |- CC = U. J |
| 4 | 3 | restid | |- ( J e. ( TopOn ` CC ) -> ( J |`t CC ) = J ) |
| 5 | 2 4 | ax-mp | |- ( J |`t CC ) = J |
| 6 | recn | |- ( y e. RR -> y e. CC ) |
|
| 7 | addcl | |- ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC ) |
|
| 8 | 6 7 | sylan2 | |- ( ( x e. CC /\ y e. RR ) -> ( x + y ) e. CC ) |
| 9 | ssid | |- CC C_ CC |
|
| 10 | 1 8 9 | reperflem | |- ( J |`t CC ) e. Perf |
| 11 | 5 10 | eqeltrri | |- J e. Perf |