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

Metamath Proof Explorer

Theorem limsupbnd1f

Description: If a sequence is eventually at most A , then the limsup is also at most A . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupbnd1f.1 
|- F/_ j F
limsupbnd1f.2 
|- ( ph -> B C_ RR )
limsupbnd1f.3 
|- ( ph -> F : B --> RR* )
limsupbnd1f.4 
|- ( ph -> A e. RR* )
limsupbnd1f.5 
|- ( ph -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ A ) )
Assertion limsupbnd1f 
|- ( ph -> ( limsup ` F ) <_ A )

Proof

Step Hyp Ref Expression
1 limsupbnd1f.1 
 |-  F/_ j F
2 limsupbnd1f.2 
 |-  ( ph -> B C_ RR )
3 limsupbnd1f.3 
 |-  ( ph -> F : B --> RR* )
4 limsupbnd1f.4 
 |-  ( ph -> A e. RR* )
5 limsupbnd1f.5 
 |-  ( ph -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ A ) )
6 breq1 
 |-  ( k = i -> ( k <_ j <-> i <_ j ) )
7 6 imbi1d 
 |-  ( k = i -> ( ( k <_ j -> ( F ` j ) <_ A ) <-> ( i <_ j -> ( F ` j ) <_ A ) ) )
8 7 ralbidv 
 |-  ( k = i -> ( A. j e. B ( k <_ j -> ( F ` j ) <_ A ) <-> A. j e. B ( i <_ j -> ( F ` j ) <_ A ) ) )
9 nfv 
 |-  F/ l ( i <_ j -> ( F ` j ) <_ A )
10 nfv 
 |-  F/ j i <_ l
11 nfcv 
 |-  F/_ j l
12 1 11 nffv 
 |-  F/_ j ( F ` l )
13 nfcv 
 |-  F/_ j <_
14 nfcv 
 |-  F/_ j A
15 12 13 14 nfbr 
 |-  F/ j ( F ` l ) <_ A
16 10 15 nfim 
 |-  F/ j ( i <_ l -> ( F ` l ) <_ A )
17 breq2 
 |-  ( j = l -> ( i <_ j <-> i <_ l ) )
18 fveq2 
 |-  ( j = l -> ( F ` j ) = ( F ` l ) )
19 18 breq1d 
 |-  ( j = l -> ( ( F ` j ) <_ A <-> ( F ` l ) <_ A ) )
20 17 19 imbi12d 
 |-  ( j = l -> ( ( i <_ j -> ( F ` j ) <_ A ) <-> ( i <_ l -> ( F ` l ) <_ A ) ) )
21 9 16 20 cbvralw 
 |-  ( A. j e. B ( i <_ j -> ( F ` j ) <_ A ) <-> A. l e. B ( i <_ l -> ( F ` l ) <_ A ) )
22 21 a1i 
 |-  ( k = i -> ( A. j e. B ( i <_ j -> ( F ` j ) <_ A ) <-> A. l e. B ( i <_ l -> ( F ` l ) <_ A ) ) )
23 8 22 bitrd 
 |-  ( k = i -> ( A. j e. B ( k <_ j -> ( F ` j ) <_ A ) <-> A. l e. B ( i <_ l -> ( F ` l ) <_ A ) ) )
24 23 cbvrexvw 
 |-  ( E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ A ) <-> E. i e. RR A. l e. B ( i <_ l -> ( F ` l ) <_ A ) )
25 5 24 sylib 
 |-  ( ph -> E. i e. RR A. l e. B ( i <_ l -> ( F ` l ) <_ A ) )
26 2 3 4 25 limsupbnd1 
 |-  ( ph -> ( limsup ` F ) <_ A )