Theorem liminfgval

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

	Ref	Expression
Hypothesis	liminfgval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion	liminfgval	⊢ ( 𝑀 ∈ ℝ → ( 𝐺 ‘ 𝑀 ) = inf ( ( ( 𝐹 “ ( 𝑀 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		liminfgval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2		oveq1	⊢ ( 𝑘 = 𝑀 → ( 𝑘 [,) +∞ ) = ( 𝑀 [,) +∞ ) )
3	2	imaeq2d	⊢ ( 𝑘 = 𝑀 → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝑀 [,) +∞ ) ) )
4	3	ineq1d	⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑀 [,) +∞ ) ) ∩ ℝ* ) )
5	4	infeq1d	⊢ ( 𝑘 = 𝑀 → inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = inf ( ( ( 𝐹 “ ( 𝑀 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
6		xrltso	⊢ < Or ℝ*
7	6	infex	⊢ inf ( ( ( 𝐹 “ ( 𝑀 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V
8	5 1 7	fvmpt	⊢ ( 𝑀 ∈ ℝ → ( 𝐺 ‘ 𝑀 ) = inf ( ( ( 𝐹 “ ( 𝑀 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )