Metamath Proof Explorer

Theorem limsupres

Description: The superior limit of a restriction is less than or equal to the original superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis limsupres.1 
|- ( ph -> F e. V )
Assertion limsupres 
|- ( ph -> ( limsup ` ( F |` C ) ) <_ ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 limsupres.1 
 |-  ( ph -> F e. V )
2 nfv 
 |-  F/ k ph
3 resimass 
 |-  ( ( F |` C ) " ( k [,) +oo ) ) C_ ( F " ( k [,) +oo ) )
4 3 a1i 
 |-  ( k e. RR -> ( ( F |` C ) " ( k [,) +oo ) ) C_ ( F " ( k [,) +oo ) ) )
5 4 ssrind 
 |-  ( k e. RR -> ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F " ( k [,) +oo ) ) i^i RR* ) )
6 5 adantl 
 |-  ( ( ph /\ k e. RR ) -> ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F " ( k [,) +oo ) ) i^i RR* ) )
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 6 8 sstrd 
 |-  ( ( ph /\ k e. RR ) -> ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) C_ RR* )
10 9 supxrcld 
 |-  ( ( ph /\ k e. RR ) -> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
11 8 supxrcld 
 |-  ( ( ph /\ k e. RR ) -> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
12 supxrss 
 |-  ( ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR* ) -> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
13 6 8 12 syl2anc 
 |-  ( ( ph /\ k e. RR ) -> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
14 2 10 11 13 infrnmptle 
 |-  ( ph -> inf ( ran ( k e. RR |-> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <_ inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
15 1 resexd 
 |-  ( ph -> ( F |` C ) e. _V )
16 eqid 
 |-  ( k e. RR |-> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
17 16 limsupval 
 |-  ( ( F |` C ) e. _V -> ( limsup ` ( F |` C ) ) = inf ( ran ( k e. RR |-> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
18 15 17 syl 
 |-  ( ph -> ( limsup ` ( F |` C ) ) = inf ( ran ( k e. RR |-> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
19 eqid 
 |-  ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
20 19 limsupval 
 |-  ( F e. V -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
21 1 20 syl 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
22 18 21 breq12d 
 |-  ( ph -> ( ( limsup ` ( F |` C ) ) <_ ( limsup ` F ) <-> inf ( ran ( k e. RR |-> sup ( ( ( ( F |` C ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <_ inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) ) )
23 14 22 mpbird 
 |-  ( ph -> ( limsup ` ( F |` C ) ) <_ ( limsup ` F ) )