Metamath Proof Explorer

Theorem limsupvaluzmpt

Description: The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -oo and the r.h.s. would be +oo ). (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupvaluzmpt.j 
|- F/ j ph
limsupvaluzmpt.m 
|- ( ph -> M e. ZZ )
limsupvaluzmpt.z 
|- Z = ( ZZ>= ` M )
limsupvaluzmpt.b 
|- ( ( ph /\ j e. Z ) -> B e. RR* )
Assertion limsupvaluzmpt 
|- ( ph -> ( limsup ` ( j e. Z |-> B ) ) = inf ( ran ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 limsupvaluzmpt.j 
 |-  F/ j ph
2 limsupvaluzmpt.m 
 |-  ( ph -> M e. ZZ )
3 limsupvaluzmpt.z 
 |-  Z = ( ZZ>= ` M )
4 limsupvaluzmpt.b 
 |-  ( ( ph /\ j e. Z ) -> B e. RR* )
5 1 4 fmptd2f 
 |-  ( ph -> ( j e. Z |-> B ) : Z --> RR* )
6 2 3 5 limsupvaluz 
 |-  ( ph -> ( limsup ` ( j e. Z |-> B ) ) = inf ( ran ( k e. Z |-> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR* , < ) )
7 3 uzssd3 
 |-  ( k e. Z -> ( ZZ>= ` k ) C_ Z )
8 7 resmptd 
 |-  ( k e. Z -> ( ( j e. Z |-> B ) |` ( ZZ>= ` k ) ) = ( j e. ( ZZ>= ` k ) |-> B ) )
9 8 rneqd 
 |-  ( k e. Z -> ran ( ( j e. Z |-> B ) |` ( ZZ>= ` k ) ) = ran ( j e. ( ZZ>= ` k ) |-> B ) )
10 9 supeq1d 
 |-  ( k e. Z -> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` k ) ) , RR* , < ) = sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) )
11 10 mpteq2ia 
 |-  ( k e. Z |-> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` k ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) )
12 11 a1i 
 |-  ( ph -> ( k e. Z |-> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` k ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) )
13 12 rneqd 
 |-  ( ph -> ran ( k e. Z |-> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` k ) ) , RR* , < ) ) = ran ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) )
14 13 infeq1d 
 |-  ( ph -> inf ( ran ( k e. Z |-> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR* , < ) = inf ( ran ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) , RR* , < ) )
15 6 14 eqtrd 
 |-  ( ph -> ( limsup ` ( j e. Z |-> B ) ) = inf ( ran ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) , RR* , < ) )