This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	ffvelcdmi	⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) ∈ ℝ^* )
14	1 13	syl	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) ∈ ℝ^* )