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