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
|- ( F e. V -> ( limsup ` F ) e. RR* )

Proof

Step Hyp Ref Expression
1 elex
 |-  ( F e. V -> F e. _V )
2 df-limsup
 |-  limsup = ( f e. _V |-> inf ( ran ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
3 eqid
 |-  ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
4 inss2
 |-  ( ( f " ( k [,) +oo ) ) i^i RR* ) C_ RR*
5 supxrcl
 |-  ( ( ( f " ( k [,) +oo ) ) i^i RR* ) C_ RR* -> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
6 4 5 mp1i
 |-  ( k e. RR -> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
7 3 6 fmpti
 |-  ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) : RR --> RR*
8 frn
 |-  ( ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) : RR --> RR* -> ran ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR* )
9 7 8 ax-mp
 |-  ran ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR*
10 infxrcl
 |-  ( ran ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR* -> inf ( ran ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) e. RR* )
11 9 10 mp1i
 |-  ( f e. _V -> inf ( ran ( k e. RR |-> sup ( ( ( f " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) e. RR* )
12 2 11 fmpti
 |-  limsup : _V --> RR*
13 12 ffvelrni
 |-  ( F e. _V -> ( limsup ` F ) e. RR* )
14 1 13 syl
 |-  ( F e. V -> ( limsup ` F ) e. RR* )