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