Theorem xlimrel

Description: The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Assertion	xlimrel	$$⊢\mathrm{Rel}\underset{*}{⇝}$$

Proof

Step	Hyp	Ref	Expression
1		lmrel	$$⊢\mathrm{Rel}\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
2		df-xlim	$$⊢\underset{*}{⇝}=\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
3	2	releqi	$$⊢\mathrm{Rel}\underset{*}{⇝}\leftrightarrow \mathrm{Rel}\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
4	1 3	mpbir	$$⊢\mathrm{Rel}\underset{*}{⇝}$$