Metamath Proof Explorer

Theorem limsupval3

Description: The superior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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