Metamath Proof Explorer

Theorem limsuplt2

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

Ref Expression
Hypotheses limsuplt2.1 
|- ( ph -> B C_ RR )
limsuplt2.2 
|- ( ph -> F : B --> RR* )
limsuplt2.3 
|- ( ph -> A e. RR* )
Assertion limsuplt2 
|- ( ph -> ( ( limsup ` F ) < A <-> E. k e. RR sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) < A ) )

Proof

Step Hyp Ref Expression
1 limsuplt2.1 
 |-  ( ph -> B C_ RR )
2 limsuplt2.2 
 |-  ( ph -> F : B --> RR* )
3 limsuplt2.3 
 |-  ( 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 limsuplt 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( ( limsup ` F ) < A <-> E. i e. RR ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) < A ) )
6 1 2 3 5 syl3anc 
 |-  ( ph -> ( ( limsup ` F ) < A <-> E. i e. RR ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) < A ) )
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 breq1d 
 |-  ( ( ph /\ i e. RR ) -> ( ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) < A <-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) < A ) )
17 16 rexbidva 
 |-  ( ph -> ( E. i e. RR ( ( j e. RR |-> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` i ) < A <-> E. i e. RR sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) < A ) )
18 oveq1 
 |-  ( i = k -> ( i [,) +oo ) = ( k [,) +oo ) )
19 18 imaeq2d 
 |-  ( i = k -> ( F " ( i [,) +oo ) ) = ( F " ( k [,) +oo ) ) )
20 19 ineq1d 
 |-  ( i = k -> ( ( F " ( i [,) +oo ) ) i^i RR* ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
21 20 supeq1d 
 |-  ( i = k -> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
22 21 breq1d 
 |-  ( i = k -> ( sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) < A <-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) < A ) )
23 22 cbvrexvw 
 |-  ( E. i e. RR sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) < A <-> E. k e. RR sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) < A )
24 23 a1i 
 |-  ( ph -> ( E. i e. RR sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) < A <-> E. k e. RR sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) < A ) )
25 6 17 24 3bitrd 
 |-  ( ph -> ( ( limsup ` F ) < A <-> E. k e. RR sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) < A ) )