Metamath Proof Explorer

Theorem xlimrel

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

Ref Expression
Assertion xlimrel 
|- Rel ~~>*

Proof

Step Hyp Ref Expression
1 lmrel 
 |-  Rel ( ~~>t ` ( ordTop ` <_ ) )
2 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
3 2 releqi 
 |-  ( Rel ~~>* <-> Rel ( ~~>t ` ( ordTop ` <_ ) ) )
4 1 3 mpbir 
 |-  Rel ~~>*