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* , < ) )