Metamath Proof Explorer

Theorem liminfval5

Description: The inferior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupval5.1 ⊢ Ⅎ 𝑘 𝜑
limsupval5.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
limsupval5.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
limsupval5.4 ⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) )
Assertion liminfval5 ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 limsupval5.1 ⊢ Ⅎ 𝑘 𝜑
2 limsupval5.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 limsupval5.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4 limsupval5.4 ⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) )
5 3 2 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
6 eqid ⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
7 6 liminfval ⊢ ( 𝐹 ∈ V → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
8 5 7 syl ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
9 4 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) )
10 3 fimassd ⊢ ( 𝜑 → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ⊆ ℝ* )
11 dfss2 ⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ⊆ ℝ* ↔ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
12 10 11 sylib ⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
13 12 eqcomd ⊢ ( 𝜑 → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
15 14 infeq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) = inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
16 1 15 mpteq2da ⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
17 9 16 eqtr2d ⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = 𝐺 )
18 17 rneqd ⊢ ( 𝜑 → ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran 𝐺 )
19 18 supeq1d ⊢ ( 𝜑 → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = sup ( ran 𝐺 , ℝ* , < ) )
20 8 19 eqtrd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ* , < ) )