Metamath Proof Explorer

Theorem limsupval

Description: The superior limit of an infinite sequence F of extended real numbers, which is the infimum of the set of suprema of all upper infinite subsequences of F . Definition 12-4.1 of Gleason p. 175. (Contributed by NM, 26-Oct-2005) (Revised by AV, 12-Sep-2014)

Ref Expression
Hypothesis limsupval.1 
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
Assertion limsupval 
|- ( F e. V -> ( limsup ` F ) = inf ( ran G , RR* , < ) )

Proof

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