Definition df-xlim

Description: Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Assertion	df-xlim	$$⊢\underset{*}{⇝}=\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clsxlim	$$class\underset{*}{⇝}$$
1		clm	$$class\underset{t}{⇝}$$
2		cordt	$$class\mathrm{ordTop}$$
3		cle	$$class\le$$
4	3 2	cfv	$$class\mathrm{ordTop}\left(\le \right)$$
5	4 1	cfv	$$class\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
6	0 5	wceq	$$wff\underset{*}{⇝}=\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$