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

Metamath Proof Explorer

Theorem limsupcli

Description: Closure of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis limsupcli.1 ⊢ 𝐹 ∈ 𝑉
Assertion limsupcli ( lim sup ‘ 𝐹 ) ∈ ℝ*

Proof

Step Hyp Ref Expression
1 limsupcli.1 ⊢ 𝐹 ∈ 𝑉
2 limsupcl ⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
3 1 2 ax-mp ⊢ ( lim sup ‘ 𝐹 ) ∈ ℝ*