Theorem liminfvald

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

	Ref	Expression
Hypotheses	liminfvald.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	liminfvald.2	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion	liminfvald	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		liminfvald.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		liminfvald.2	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
3	2	liminfval	⊢ ( 𝐹 ∈ 𝑉 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ* , < ) )
4	1 3	syl	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ* , < ) )