Metamath Proof Explorer

Theorem limsuplesup

Description: An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsuplesup.1 
|- ( ph -> F e. V )
limsuplesup.2 
|- ( ph -> K e. RR )
Assertion limsuplesup 
|- ( ph -> ( limsup ` F ) <_ sup ( ( ( F " ( K [,) +oo ) ) i^i RR* ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 limsuplesup.1 
 |-  ( ph -> F e. V )
2 limsuplesup.2 
 |-  ( ph -> K e. 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 3 limsupval 
 |-  ( F e. V -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
5 1 4 syl 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
6 nfv 
 |-  F/ k ph
7 inss2 
 |-  ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR*
8 7 a1i 
 |-  ( ( ph /\ k e. RR ) -> ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR* )
9 8 supxrcld 
 |-  ( ( ph /\ k e. RR ) -> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
10 inss2 
 |-  ( ( F " ( K [,) +oo ) ) i^i RR* ) C_ RR*
11 10 a1i 
 |-  ( ph -> ( ( F " ( K [,) +oo ) ) i^i RR* ) C_ RR* )
12 11 supxrcld 
 |-  ( ph -> sup ( ( ( F " ( K [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
13 oveq1 
 |-  ( k = K -> ( k [,) +oo ) = ( K [,) +oo ) )
14 13 imaeq2d 
 |-  ( k = K -> ( F " ( k [,) +oo ) ) = ( F " ( K [,) +oo ) ) )
15 14 ineq1d 
 |-  ( k = K -> ( ( F " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( K [,) +oo ) ) i^i RR* ) )
16 15 supeq1d 
 |-  ( k = K -> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( K [,) +oo ) ) i^i RR* ) , RR* , < ) )
17 6 9 2 12 16 infxrlbrnmpt2 
 |-  ( ph -> inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <_ sup ( ( ( F " ( K [,) +oo ) ) i^i RR* ) , RR* , < ) )
18 5 17 eqbrtrd 
 |-  ( ph -> ( limsup ` F ) <_ sup ( ( ( F " ( K [,) +oo ) ) i^i RR* ) , RR* , < ) )