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

Metamath Proof Explorer

Theorem climdm

Description: Two ways to express that a function has a limit. (The expression ( ~>F ) is sometimes useful as a shorthand for "the unique limit of the function F "). (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion climdm ⊢ F ∈ dom ⁡ ⇝ ↔ F ⇝ ⇝ ⁡ F

Proof

Step Hyp Ref Expression
1 fclim ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ
2 ffun ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ → Fun ⁡ ⇝
3 funfvbrb ⊢ Fun ⁡ ⇝ → F ∈ dom ⁡ ⇝ ↔ F ⇝ ⇝ ⁡ F
4 1 2 3 mp2b ⊢ F ∈ dom ⁡ ⇝ ↔ F ⇝ ⇝ ⁡ F