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

Metamath Proof Explorer

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 sselid ⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )