Step |
Hyp |
Ref |
Expression |
1 |
|
limsupval.1 |
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) |
2 |
|
elex |
|- ( F e. V -> F e. _V ) |
3 |
|
imaeq1 |
|- ( x = F -> ( x " ( k [,) +oo ) ) = ( F " ( k [,) +oo ) ) ) |
4 |
3
|
ineq1d |
|- ( x = F -> ( ( x " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) ) |
5 |
4
|
supeq1d |
|- ( x = F -> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) |
6 |
5
|
mpteq2dv |
|- ( x = F -> ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) ) |
7 |
6 1
|
eqtr4di |
|- ( x = F -> ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = G ) |
8 |
7
|
rneqd |
|- ( x = F -> ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran G ) |
9 |
8
|
infeq1d |
|- ( x = F -> inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) = inf ( ran G , RR* , < ) ) |
10 |
|
df-limsup |
|- limsup = ( x e. _V |-> inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) ) |
11 |
|
xrltso |
|- < Or RR* |
12 |
11
|
infex |
|- inf ( ran G , RR* , < ) e. _V |
13 |
9 10 12
|
fvmpt |
|- ( F e. _V -> ( limsup ` F ) = inf ( ran G , RR* , < ) ) |
14 |
2 13
|
syl |
|- ( F e. V -> ( limsup ` F ) = inf ( ran G , RR* , < ) ) |