Metamath Proof Explorer


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 jφ
limsupubuzmpt.z Z=M
limsupubuzmpt.b φjZB
limsupubuzmpt.n φlim supjZB+∞
Assertion limsupubuzmpt φxjZBx

Proof

Step Hyp Ref Expression
1 limsupubuzmpt.j jφ
2 limsupubuzmpt.z Z=M
3 limsupubuzmpt.b φjZB
4 limsupubuzmpt.n φlim supjZB+∞
5 nfmpt1 _jjZB
6 eqid jZB=jZB
7 1 3 6 fmptdf φjZB:Z
8 5 2 7 4 limsupubuz φyjZjZBjy
9 6 a1i φjZB=jZB
10 9 3 fvmpt2d φjZjZBj=B
11 10 breq1d φjZjZBjyBy
12 1 11 ralbida φjZjZBjyjZBy
13 12 rexbidv φyjZjZBjyyjZBy
14 8 13 mpbid φyjZBy
15 breq2 y=xByBx
16 15 ralbidv y=xjZByjZBx
17 16 cbvrexvw yjZByxjZBx
18 14 17 sylib φxjZBx