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\in \mathrm{dom}⇝\leftrightarrow F⇝⇝\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fclim	$$⊢⇝:\mathrm{dom}⇝⟶ℂ$$
2		ffun	$$⊢⇝:\mathrm{dom}⇝⟶ℂ\to \mathrm{Fun}⇝$$
3		funfvbrb	$$⊢\mathrm{Fun}⇝\to \left(F\in \mathrm{dom}⇝\leftrightarrow F⇝⇝\left(F\right)\right)$$
4	1 2 3	mp2b	$$⊢F\in \mathrm{dom}⇝\leftrightarrow F⇝⇝\left(F\right)$$