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 \mathrm{dom}F\subseteq ℝ$$

Proof

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