Theorem liminfcl

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

	Ref	Expression
Assertion	liminfcl	⊢ ( 𝐹 ∈ 𝑉 → ( lim inf ‘ 𝐹 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2	1	liminfval	⊢ ( 𝐹 ∈ 𝑉 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
3		nfv	⊢ Ⅎ 𝑘 𝐹 ∈ 𝑉
4		inss2	⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
5		infxrcl	⊢ ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* → inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
6	4 5	ax-mp	⊢ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
7	6	a1i	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑘 ∈ ℝ ) → inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
8	3 1 7	rnmptssd	⊢ ( 𝐹 ∈ 𝑉 → ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ* )
9	8	supxrcld	⊢ ( 𝐹 ∈ 𝑉 → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ∈ ℝ* )
10	2 9	eqeltrd	⊢ ( 𝐹 ∈ 𝑉 → ( lim inf ‘ 𝐹 ) ∈ ℝ* )