This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( ( ( 𝐹 “ ( 𝑀 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )