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

Metamath Proof Explorer

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 ‘ 𝐹 ) ∈ ℝ* )