Theorem rlimpm

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

	Ref	Expression
Assertion	rlimpm	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		df-rlim	⊢ ⇝𝑟 = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) }
2		opabssxp	⊢ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) } ⊆ ( ( ℂ ↑pm ℝ ) × ℂ )
3	1 2	eqsstri	⊢ ⇝𝑟 ⊆ ( ( ℂ ↑pm ℝ ) × ℂ )
4		dmss	⊢ ( ⇝𝑟 ⊆ ( ( ℂ ↑pm ℝ ) × ℂ ) → dom ⇝𝑟 ⊆ dom ( ( ℂ ↑pm ℝ ) × ℂ ) )
5	3 4	ax-mp	⊢ dom ⇝𝑟 ⊆ dom ( ( ℂ ↑pm ℝ ) × ℂ )
6		dmxpss	⊢ dom ( ( ℂ ↑pm ℝ ) × ℂ ) ⊆ ( ℂ ↑pm ℝ )
7	5 6	sstri	⊢ dom ⇝𝑟 ⊆ ( ℂ ↑pm ℝ )
8		rlimrel	⊢ Rel ⇝𝑟
9	8	releldmi	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ dom ⇝𝑟 )
10	7 9	sseldi	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )