rlimpm

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

		Ref	Expression
	Assertion	rlimpm	$⊢ F \underset{ℝ}{⇝} A \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$

Step	Hyp	Ref	Expression
1		df-rlim	$⊢ \underset{ℝ}{⇝} = \{⟨f, x⟩ \| ((f \in (ℂ ↑_{𝑝𝑚} ℝ) \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ \forall w \in dom f (z \leq w \to \|f (w) - x\| < y))\}$
2		opabssxp	$⊢ \{⟨f, x⟩ \| ((f \in (ℂ ↑_{𝑝𝑚} ℝ) \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ \forall w \in dom f (z \leq w \to \|f (w) - x\| < y))\} \subseteq (ℂ ↑_{𝑝𝑚} ℝ) \times ℂ$
3	1 2	eqsstri	$⊢ \underset{ℝ}{⇝} \subseteq (ℂ ↑_{𝑝𝑚} ℝ) \times ℂ$
4		dmss	$⊢ \underset{ℝ}{⇝} \subseteq (ℂ ↑_{𝑝𝑚} ℝ) \times ℂ \to dom \underset{ℝ}{⇝} \subseteq dom ((ℂ ↑_{𝑝𝑚} ℝ) \times ℂ)$
5	3 4	ax-mp	$⊢ dom \underset{ℝ}{⇝} \subseteq dom ((ℂ ↑_{𝑝𝑚} ℝ) \times ℂ)$
6		dmxpss	$⊢ dom ((ℂ ↑_{𝑝𝑚} ℝ) \times ℂ) \subseteq ℂ ↑_{𝑝𝑚} ℝ$
7	5 6	sstri	$⊢ dom \underset{ℝ}{⇝} \subseteq ℂ ↑_{𝑝𝑚} ℝ$
8		rlimrel	$⊢ Rel \underset{ℝ}{⇝}$
9	8	releldmi	$⊢ F \underset{ℝ}{⇝} A \to F \in dom \underset{ℝ}{⇝}$
10	7 9	sselid	$⊢ F \underset{ℝ}{⇝} A \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$

Metamath Proof Explorer