Theorem liminfgval

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

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

Proof

Step	Hyp	Ref	Expression
1		liminfgval.1	|- G = ( k e. RR |-> inf ( ( ( 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	infeq1d	|- ( k = M -> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = inf ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) )
6		xrltso	|- < Or RR*
7	6	infex	|- inf ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V
8	5 1 7	fvmpt	|- ( M e. RR -> ( G ` M ) = inf ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) )