This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsuppnf

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 limsuppnf.j 
 |-  F/_ j F
2 limsuppnf.a 
 |-  ( ph -> A C_ RR )
3 limsuppnf.f 
 |-  ( ph -> F : A --> RR* )
4 nfcv 
 |-  F/_ l F
5 4 2 3 limsuppnflem 
 |-  ( ph -> ( ( limsup ` F ) = +oo <-> A. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) ) )
6 breq1 
 |-  ( i = k -> ( i <_ l <-> k <_ l ) )
7 6 anbi1d 
 |-  ( i = k -> ( ( i <_ l /\ y <_ ( F ` l ) ) <-> ( k <_ l /\ y <_ ( F ` l ) ) ) )
8 7 rexbidv 
 |-  ( i = k -> ( E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> E. l e. A ( k <_ l /\ y <_ ( F ` l ) ) ) )
9 nfv 
 |-  F/ j k <_ l
10 nfcv 
 |-  F/_ j y
11 nfcv 
 |-  F/_ j <_
12 nfcv 
 |-  F/_ j l
13 1 12 nffv 
 |-  F/_ j ( F ` l )
14 10 11 13 nfbr 
 |-  F/ j y <_ ( F ` l )
15 9 14 nfan 
 |-  F/ j ( k <_ l /\ y <_ ( F ` l ) )
16 nfv 
 |-  F/ l ( k <_ j /\ y <_ ( F ` j ) )
17 breq2 
 |-  ( l = j -> ( k <_ l <-> k <_ j ) )
18 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
19 18 breq2d 
 |-  ( l = j -> ( y <_ ( F ` l ) <-> y <_ ( F ` j ) ) )
20 17 19 anbi12d 
 |-  ( l = j -> ( ( k <_ l /\ y <_ ( F ` l ) ) <-> ( k <_ j /\ y <_ ( F ` j ) ) ) )
21 15 16 20 cbvrexw 
 |-  ( E. l e. A ( k <_ l /\ y <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) )
22 21 a1i 
 |-  ( i = k -> ( E. l e. A ( k <_ l /\ y <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
23 8 22 bitrd 
 |-  ( i = k -> ( E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
24 23 cbvralvw 
 |-  ( A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) )
25 24 a1i 
 |-  ( y = x -> ( A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
26 breq1 
 |-  ( y = x -> ( y <_ ( F ` j ) <-> x <_ ( F ` j ) ) )
27 26 anbi2d 
 |-  ( y = x -> ( ( k <_ j /\ y <_ ( F ` j ) ) <-> ( k <_ j /\ x <_ ( F ` j ) ) ) )
28 27 rexbidv 
 |-  ( y = x -> ( E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) <-> E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
29 28 ralbidv 
 |-  ( y = x -> ( A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
30 25 29 bitrd 
 |-  ( y = x -> ( A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
31 30 cbvralvw 
 |-  ( A. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
32 31 a1i 
 |-  ( ph -> ( A. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
33 5 32 bitrd 
 |-  ( ph -> ( ( limsup ` F ) = +oo <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )