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

Metamath Proof Explorer

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 ( 𝐹 ⇝𝑟 𝐴 → dom 𝐹 ⊆ ℝ )

Proof

Step Hyp Ref Expression
1 rlimpm ⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
2 cnex ⊢ ℂ ∈ V
3 reex ⊢ ℝ ∈ V
4 2 3 elpm2 ⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
5 4 simprbi ⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → dom 𝐹 ⊆ ℝ )
6 1 5 syl ⊢ ( 𝐹 ⇝𝑟 𝐴 → dom 𝐹 ⊆ ℝ )