Metamath Proof Explorer

Theorem xlimfun

Description: The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Assertion xlimfun 
|- Fun ~~>*

Proof

Step Hyp Ref Expression
1 xrhaus 
 |-  ( ordTop ` <_ ) e. Haus
2 lmfun 
 |-  ( ( ordTop ` <_ ) e. Haus -> Fun ( ~~>t ` ( ordTop ` <_ ) ) )
3 1 2 ax-mp 
 |-  Fun ( ~~>t ` ( ordTop ` <_ ) )
4 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
5 4 funeqi 
 |-  ( Fun ~~>* <-> Fun ( ~~>t ` ( ordTop ` <_ ) ) )
6 3 5 mpbir 
 |-  Fun ~~>*