Theorem cnperf

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

	Ref	Expression
Hypothesis	recld2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnperf	$$⊢J\in \mathrm{Perf}$$

Proof

Step	Hyp	Ref	Expression
1		recld2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	cnfldtopon	$$⊢J\in \mathrm{TopOn}\left(ℂ\right)$$
3	2	toponunii	$$⊢ℂ=\bigcup J$$
4	3	restid	$$⊢J\in \mathrm{TopOn}\left(ℂ\right)\to J{\upharpoonright }_{𝑡}ℂ=J$$
5	2 4	ax-mp	$$⊢J{\upharpoonright }_{𝑡}ℂ=J$$
6		recn	$$⊢y\in ℝ\to y\in ℂ$$
7		addcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x+y\in ℂ$$
8	6 7	sylan2	$$⊢\left(x\in ℂ\wedge y\in ℝ\right)\to x+y\in ℂ$$
9		ssid	$$⊢ℂ\subseteq ℂ$$
10	1 8 9	reperflem	$$⊢J{\upharpoonright }_{𝑡}ℂ\in \mathrm{Perf}$$
11	5 10	eqeltrri	$$⊢J\in \mathrm{Perf}$$