cnperf

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

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

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

Metamath Proof Explorer