Definition df-xlim

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

	Ref	Expression
Assertion	df-xlim	⊢ ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clsxlim	⊢ ~~>*
1		clm	⊢ ⇝𝑡
2		cordt	⊢ ordTop
3		cle	⊢ ≤
4	3 2	cfv	⊢ ( ordTop ‘ ≤ )
5	4 1	cfv	⊢ ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )
6	0 5	wceq	⊢ ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )