Theorem limsupval

Description: The superior limit of an infinite sequence F of extended real numbers, which is the infimum of the set of suprema of all upper infinite subsequences of F . Definition 12-4.1 of Gleason p. 175. (Contributed by NM, 26-Oct-2005) (Revised by AV, 12-Sep-2014)

	Ref	Expression
Hypothesis	limsupval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion	limsupval	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2		elex	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
3		imaeq1	⊢ ( 𝑥 = 𝐹 → ( 𝑥 “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
4	3	ineq1d	⊢ ( 𝑥 = 𝐹 → ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
5	4	supeq1d	⊢ ( 𝑥 = 𝐹 → sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
6	5	mpteq2dv	⊢ ( 𝑥 = 𝐹 → ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
7	6 1	eqtr4di	⊢ ( 𝑥 = 𝐹 → ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = 𝐺 )
8	7	rneqd	⊢ ( 𝑥 = 𝐹 → ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran 𝐺 )
9	8	infeq1d	⊢ ( 𝑥 = 𝐹 → inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran 𝐺 , ℝ* , < ) )
10		df-limsup	⊢ lim sup = ( 𝑥 ∈ V ↦ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
11		xrltso	⊢ < Or ℝ*
12	11	infex	⊢ inf ( ran 𝐺 , ℝ* , < ) ∈ V
13	9 10 12	fvmpt	⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
14	2 13	syl	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )