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* )