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

Metamath Proof Explorer

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 = TopOpen (ℂ_{fld})$
	Assertion	reperf	$⊢ J ↾_{𝑡} ℝ \in Perf$

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