Theorem xlimfun

Description: The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Assertion	xlimfun	$$⊢\mathrm{Fun}\underset{*}{⇝}$$

Proof

Step	Hyp	Ref	Expression
1		xrhaus	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{Haus}$$
2		lmfun	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{Haus}\to \mathrm{Fun}\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
3	1 2	ax-mp	$$⊢\mathrm{Fun}\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
4		df-xlim	$$⊢\underset{*}{⇝}=\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
5	4	funeqi	$$⊢\mathrm{Fun}\underset{*}{⇝}\leftrightarrow \mathrm{Fun}\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
6	3 5	mpbir	$$⊢\mathrm{Fun}\underset{*}{⇝}$$