Metamath Proof Explorer

Theorem limsupge

Description: The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupge.b 
|- ( ph -> B C_ RR )
limsupge.f 
|- ( ph -> F : B --> RR* )
limsupge.a 
|- ( ph -> A e. RR* )
Assertion limsupge 
|- ( ph -> ( A <_ ( limsup ` F ) <-> A. k e. RR A <_ sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )

Proof

Step Hyp Ref Expression
1 limsupge.b 
 |-  ( ph -> B C_ RR )
2 limsupge.f 
 |-  ( ph -> F : B --> RR* )
3 limsupge.a 
 |-  ( ph -> A e. RR* )
4 eqid 
 |-  ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) )
5 4 limsuple 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ ( limsup ` F ) <-> A. i e. RR A <_ ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) ) )
6 1 2 3 5 syl3anc 
 |-  ( ph -> ( A <_ ( limsup ` F ) <-> A. i e. RR A <_ ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) ) )
7 oveq1 
 |-  ( j = i -> ( j [,) +oo ) = ( i [,) +oo ) )
8 7 imaeq2d 
 |-  ( j = i -> ( F " ( j [,) +oo ) ) = ( F " ( i [,) +oo ) ) )
9 8 ineq1d 
 |-  ( j = i -> ( ( F " ( j [,) +oo ) ) i^i RR* ) = ( ( F " ( i [,) +oo ) ) i^i RR* ) )
10 9 supeq1d 
 |-  ( j = i -> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
11 simpr 
 |-  ( ( ph /\ i e. RR ) -> i e. RR )
12 xrltso 
 |-  < Or RR*
13 12 supex 
 |-  sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V
14 13 a1i 
 |-  ( ( ph /\ i e. RR ) -> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V )
15 4 10 11 14 fvmptd3 
 |-  ( ( ph /\ i e. RR ) -> ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) = sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
16 15 breq2d 
 |-  ( ( ph /\ i e. RR ) -> ( A <_ ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) <-> A <_ sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
17 16 ralbidva 
 |-  ( ph -> ( A. i e. RR A <_ ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) <-> A. i e. RR A <_ sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
18 6 17 bitrd 
 |-  ( ph -> ( A <_ ( limsup ` F ) <-> A. i e. RR A <_ sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
19 oveq1 
 |-  ( i = k -> ( i [,) +oo ) = ( k [,) +oo ) )
20 19 imaeq2d 
 |-  ( i = k -> ( F " ( i [,) +oo ) ) = ( F " ( k [,) +oo ) ) )
21 20 ineq1d 
 |-  ( i = k -> ( ( F " ( i [,) +oo ) ) i^i RR* ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
22 21 supeq1d 
 |-  ( i = k -> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
23 22 breq2d 
 |-  ( i = k -> ( A <_ sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <-> A <_ sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
24 23 cbvralvw 
 |-  ( A. i e. RR A <_ sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <-> A. k e. RR A <_ sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
25 24 a1i 
 |-  ( ph -> ( A. i e. RR A <_ sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <-> A. k e. RR A <_ sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
26 18 25 bitrd 
 |-  ( ph -> ( A <_ ( limsup ` F ) <-> A. k e. RR A <_ sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )