Metamath Proof Explorer

Theorem limsupmnf

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupmnf.j 
|- F/_ j F
limsupmnf.a 
|- ( ph -> A C_ RR )
limsupmnf.f 
|- ( ph -> F : A --> RR* )
Assertion limsupmnf 
|- ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )

Proof

Step Hyp Ref Expression
1 limsupmnf.j 
 |-  F/_ j F
2 limsupmnf.a 
 |-  ( ph -> A C_ RR )
3 limsupmnf.f 
 |-  ( ph -> F : A --> RR* )
4 eqid 
 |-  ( i e. RR |-> sup ( ( F " ( i [,) +oo ) ) , RR* , < ) ) = ( i e. RR |-> sup ( ( F " ( i [,) +oo ) ) , RR* , < ) )
5 2 3 4 limsupmnflem 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> A. y e. RR E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) ) )
6 breq2 
 |-  ( y = x -> ( ( F ` l ) <_ y <-> ( F ` l ) <_ x ) )
7 6 imbi2d 
 |-  ( y = x -> ( ( i <_ l -> ( F ` l ) <_ y ) <-> ( i <_ l -> ( F ` l ) <_ x ) ) )
8 7 ralbidv 
 |-  ( y = x -> ( A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> A. l e. A ( i <_ l -> ( F ` l ) <_ x ) ) )
9 8 rexbidv 
 |-  ( y = x -> ( E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ x ) ) )
10 breq1 
 |-  ( i = k -> ( i <_ l <-> k <_ l ) )
11 10 imbi1d 
 |-  ( i = k -> ( ( i <_ l -> ( F ` l ) <_ x ) <-> ( k <_ l -> ( F ` l ) <_ x ) ) )
12 11 ralbidv 
 |-  ( i = k -> ( A. l e. A ( i <_ l -> ( F ` l ) <_ x ) <-> A. l e. A ( k <_ l -> ( F ` l ) <_ x ) ) )
13 nfv 
 |-  F/ j k <_ l
14 nfcv 
 |-  F/_ j l
15 1 14 nffv 
 |-  F/_ j ( F ` l )
16 nfcv 
 |-  F/_ j <_
17 nfcv 
 |-  F/_ j x
18 15 16 17 nfbr 
 |-  F/ j ( F ` l ) <_ x
19 13 18 nfim 
 |-  F/ j ( k <_ l -> ( F ` l ) <_ x )
20 nfv 
 |-  F/ l ( k <_ j -> ( F ` j ) <_ x )
21 breq2 
 |-  ( l = j -> ( k <_ l <-> k <_ j ) )
22 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
23 22 breq1d 
 |-  ( l = j -> ( ( F ` l ) <_ x <-> ( F ` j ) <_ x ) )
24 21 23 imbi12d 
 |-  ( l = j -> ( ( k <_ l -> ( F ` l ) <_ x ) <-> ( k <_ j -> ( F ` j ) <_ x ) ) )
25 19 20 24 cbvralw 
 |-  ( A. l e. A ( k <_ l -> ( F ` l ) <_ x ) <-> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
26 25 a1i 
 |-  ( i = k -> ( A. l e. A ( k <_ l -> ( F ` l ) <_ x ) <-> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
27 12 26 bitrd 
 |-  ( i = k -> ( A. l e. A ( i <_ l -> ( F ` l ) <_ x ) <-> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
28 27 cbvrexvw 
 |-  ( E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ x ) <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
29 28 a1i 
 |-  ( y = x -> ( E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ x ) <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
30 9 29 bitrd 
 |-  ( y = x -> ( E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
31 30 cbvralvw 
 |-  ( A. y e. RR E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
32 31 a1i 
 |-  ( ph -> ( A. y e. RR E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
33 5 32 bitrd 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )