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	⊢ ( 𝐹 ∈ dom ~~>* ↔ 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		xlimfun	⊢ Fun ~~>*
2		funfvbrb	⊢ ( Fun ~~>* → ( 𝐹 ∈ dom ~~>* ↔ 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) ) )
3	1 2	ax-mp	⊢ ( 𝐹 ∈ dom ~~>* ↔ 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )