Metamath Proof Explorer

Theorem limsuppnfd

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 limsuppnfd.j 
|- F/_ j F
limsuppnfd.a 
|- ( ph -> A C_ RR )
limsuppnfd.f 
|- ( ph -> F : A --> RR* )
limsuppnfd.u 
|- ( ph -> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
Assertion limsuppnfd 
|- ( ph -> ( limsup ` F ) = +oo )

Proof

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