Metamath Proof Explorer

Definition df-xlim

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

Ref Expression
Assertion df-xlim 
|- ~~>* = ( ~~>t ` ( ordTop ` <_ ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsxlim 
 |-  ~~>*
1 clm 
 |-  ~~>t
2 cordt 
 |-  ordTop
3 cle 
 |-  <_
4 3 2 cfv 
 |-  ( ordTop ` <_ )
5 4 1 cfv 
 |-  ( ~~>t ` ( ordTop ` <_ ) )
6 0 5 wceq 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )