This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupgval

Description: Value of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

Ref Expression
Hypothesis limsupval.1 
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
Assertion limsupgval 
|- ( M e. RR -> ( G ` M ) = sup ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 limsupval.1 
 |-  G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2 oveq1 
 |-  ( k = M -> ( k [,) +oo ) = ( M [,) +oo ) )
3 2 imaeq2d 
 |-  ( k = M -> ( F " ( k [,) +oo ) ) = ( F " ( M [,) +oo ) ) )
4 3 ineq1d 
 |-  ( k = M -> ( ( F " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( M [,) +oo ) ) i^i RR* ) )
5 4 supeq1d 
 |-  ( k = M -> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) )
6 xrltso 
 |-  < Or RR*
7 6 supex 
 |-  sup ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V
8 5 1 7 fvmpt 
 |-  ( M e. RR -> ( G ` M ) = sup ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) )