Theorem limsupubuzmpt

Description: If the limsup is not +oo , then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupubuzmpt.j	|- F/ j ph
	limsupubuzmpt.z	|- Z = ( ZZ>= ` M )
	limsupubuzmpt.b	|- ( ( ph /\ j e. Z ) -> B e. RR )
	limsupubuzmpt.n	|- ( ph -> ( limsup ` ( j e. Z |-> B ) ) =/= +oo )
Assertion	limsupubuzmpt	|- ( ph -> E. x e. RR A. j e. Z B <_ x )

Proof

Step	Hyp	Ref	Expression
1		limsupubuzmpt.j	|- F/ j ph
2		limsupubuzmpt.z	|- Z = ( ZZ>= ` M )
3		limsupubuzmpt.b	|- ( ( ph /\ j e. Z ) -> B e. RR )
4		limsupubuzmpt.n	|- ( ph -> ( limsup ` ( j e. Z |-> B ) ) =/= +oo )
5		nfmpt1	|- F/_ j ( j e. Z |-> B )
6		eqid	|- ( j e. Z |-> B ) = ( j e. Z |-> B )
7	1 3 6	fmptdf	|- ( ph -> ( j e. Z |-> B ) : Z --> RR )
8	5 2 7 4	limsupubuz	|- ( ph -> E. y e. RR A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y )
9	6	a1i	|- ( ph -> ( j e. Z |-> B ) = ( j e. Z |-> B ) )
10	9 3	fvmpt2d	|- ( ( ph /\ j e. Z ) -> ( ( j e. Z |-> B ) ` j ) = B )
11	10	breq1d	|- ( ( ph /\ j e. Z ) -> ( ( ( j e. Z |-> B ) ` j ) <_ y <-> B <_ y ) )
12	1 11	ralbida	|- ( ph -> ( A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y <-> A. j e. Z B <_ y ) )
13	12	rexbidv	|- ( ph -> ( E. y e. RR A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y <-> E. y e. RR A. j e. Z B <_ y ) )
14	8 13	mpbid	|- ( ph -> E. y e. RR A. j e. Z B <_ y )
15		breq2	|- ( y = x -> ( B <_ y <-> B <_ x ) )
16	15	ralbidv	|- ( y = x -> ( A. j e. Z B <_ y <-> A. j e. Z B <_ x ) )
17	16	cbvrexvw	|- ( E. y e. RR A. j e. Z B <_ y <-> E. x e. RR A. j e. Z B <_ x )
18	14 17	sylib	|- ( ph -> E. x e. RR A. j e. Z B <_ x )