Theorem liminfvald

Description: The inferior limit of a set F . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfvald.1	|- ( ph -> F e. V )
	liminfvald.2	|- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
Assertion	liminfvald	|- ( ph -> ( liminf ` F ) = sup ( ran G , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		liminfvald.1	|- ( ph -> F e. V )
2		liminfvald.2	|- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
3	2	liminfval	|- ( F e. V -> ( liminf ` F ) = sup ( ran G , RR* , < ) )
4	1 3	syl	|- ( ph -> ( liminf ` F ) = sup ( ran G , RR* , < ) )