Theorem reperf

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

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

Proof

Step	Hyp	Ref	Expression
1		recld2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		readdcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+y\in ℝ$$
3		ax-resscn	$$⊢ℝ\subseteq ℂ$$
4	1 2 3	reperflem	$$⊢J{\upharpoonright }_{𝑡}ℝ\in \mathrm{Perf}$$