This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnperf

Description: The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016)

Ref Expression
Hypothesis recld2.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion cnperf 𝐽 ∈ Perf

Proof

Step Hyp Ref Expression
1 recld2.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
3 2 toponunii ⊢ ℂ = ∪ 𝐽
4 3 restid ⊢ ( 𝐽 ∈ ( TopOn ‘ ℂ ) → ( 𝐽 ↾t ℂ ) = 𝐽 )
5 2 4 ax-mp ⊢ ( 𝐽 ↾t ℂ ) = 𝐽
6 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
7 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
8 6 7 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
9 ssid ⊢ ℂ ⊆ ℂ
10 1 8 9 reperflem ⊢ ( 𝐽 ↾t ℂ ) ∈ Perf
11 5 10 eqeltrri ⊢ 𝐽 ∈ Perf