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

Metamath Proof Explorer

Theorem rlimss

Description: Domain closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014)

		Ref	Expression
	Assertion	rlimss	$⊢ F \underset{ℝ}{⇝} A \to dom F \subseteq ℝ$

Step	Hyp	Ref	Expression
1		rlimpm	$⊢ F \underset{ℝ}{⇝} A \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
2		cnex	$⊢ ℂ \in V$
3		reex	$⊢ ℝ \in V$
4	2 3	elpm2	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
5	4	simprbi	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to dom F \subseteq ℝ$
6	1 5	syl	$⊢ F \underset{ℝ}{⇝} A \to dom F \subseteq ℝ$