Theorem liminfgf

Description: Closure of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	liminfgf.1	|- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
Assertion	liminfgf	|- G : RR --> RR*

Proof

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