Theorem limsupcl

Description: Closure of the superior limit. (Contributed by NM, 26-Oct-2005) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Assertion	limsupcl	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
2		df-limsup	⊢ lim sup = ( 𝑓 ∈ V ↦ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
3		eqid	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
4		inss2	⊢ ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
5		supxrcl	⊢ ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* → sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
6	4 5	mp1i	⊢ ( 𝑘 ∈ ℝ → sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
7	3 6	fmpti	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) : ℝ ⟶ ℝ*
8		frn	⊢ ( ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) : ℝ ⟶ ℝ* → ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ* )
9	7 8	ax-mp	⊢ ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ*
10		infxrcl	⊢ ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ* → inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ∈ ℝ* )
11	9 10	mp1i	⊢ ( 𝑓 ∈ V → inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑓 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ∈ ℝ* )
12	2 11	fmpti	⊢ lim sup : V ⟶ ℝ*
13	12	ffvelrni	⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
14	1 13	syl	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )