Theorem rlimf

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

	Ref	Expression
Assertion	rlimf	$$⊢F\underset{ℝ}{⇝}A\to F:\mathrm{dom}F⟶ℂ$$

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	simplbi	$$⊢F\in \left(ℂ{\uparrow }_{𝑝𝑚}ℝ\right)\to F:\mathrm{dom}F⟶ℂ$$
6	1 5	syl	$$⊢F\underset{ℝ}{⇝}A\to F:\mathrm{dom}F⟶ℂ$$