Theorem limsupgf

Description: Closure 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	limsupgf	|- G : RR --> RR*

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2		inss2	|- ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR*
3		supxrcl	|- ( ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR* -> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
4	2 3	mp1i	|- ( k e. RR -> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
5	1 4	fmpti	|- G : RR --> RR*