Metamath Proof Explorer

Theorem xlimcl

Description: The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Assertion xlimcl 
|- ( F ~~>* A -> A e. RR* )

Proof

Step Hyp Ref Expression
1 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
2 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
3 2 breqi 
 |-  ( F ~~>* A <-> F ( ~~>t ` ( ordTop ` <_ ) ) A )
4 3 biimpi 
 |-  ( F ~~>* A -> F ( ~~>t ` ( ordTop ` <_ ) ) A )
5 lmcl 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ F ( ~~>t ` ( ordTop ` <_ ) ) A ) -> A e. RR* )
6 1 4 5 sylancr 
 |-  ( F ~~>* A -> A e. RR* )