Metamath Proof Explorer

Theorem limsupval3

Description: The superior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupval3.1 
|- F/ k ph
limsupval3.2 
|- ( ph -> A e. V )
limsupval3.3 
|- ( ph -> F : A --> RR* )
limsupval3.4 
|- G = ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) )
Assertion limsupval3 
|- ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )

Proof

Step Hyp Ref Expression
1 limsupval3.1 
 |-  F/ k ph
2 limsupval3.2 
 |-  ( ph -> A e. V )
3 limsupval3.3 
 |-  ( ph -> F : A --> RR* )
4 limsupval3.4 
 |-  G = ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) )
5 3 2 fexd 
 |-  ( ph -> F e. _V )
6 eqid 
 |-  ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
7 6 limsupval 
 |-  ( F e. _V -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
8 5 7 syl 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
9 4 a1i 
 |-  ( ph -> G = ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) )
10 3 fimassd 
 |-  ( ph -> ( F " ( k [,) +oo ) ) C_ RR* )
11 df-ss 
 |-  ( ( F " ( k [,) +oo ) ) C_ RR* <-> ( ( F " ( k [,) +oo ) ) i^i RR* ) = ( F " ( k [,) +oo ) ) )
12 10 11 sylib 
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) = ( F " ( k [,) +oo ) ) )
13 12 eqcomd 
 |-  ( ph -> ( F " ( k [,) +oo ) ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
14 13 supeq1d 
 |-  ( ph -> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) = sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
15 14 adantr 
 |-  ( ( ph /\ k e. RR ) -> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) = sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
16 1 15 mpteq2da 
 |-  ( ph -> ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
17 9 16 eqtr2d 
 |-  ( ph -> ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = G )
18 17 rneqd 
 |-  ( ph -> ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran G )
19 18 infeq1d 
 |-  ( ph -> inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) = inf ( ran G , RR* , < ) )
20 8 19 eqtrd 
 |-  ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )