Theorem xlimdm

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 Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Assertion	xlimdm	$$⊢F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow F\underset{*}{⇝}\underset{*}{⇝}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		xlimfun	$$⊢\mathrm{Fun}\underset{*}{⇝}$$
2		funfvbrb	$$⊢\mathrm{Fun}\underset{*}{⇝}\to \left(F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow F\underset{*}{⇝}\underset{*}{⇝}\left(F\right)\right)$$
3	1 2	ax-mp	$$⊢F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow F\underset{*}{⇝}\underset{*}{⇝}\left(F\right)$$