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