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\phi$$
	limsupubuzmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	limsupubuzmpt.b	$$⊢\left(\phi \wedge j\in Z\right)\to B\in ℝ$$
	limsupubuzmpt.n	$$⊢\phi \to \mathrm{lim\; sup}\left(\left(j\in Z⟼B\right)\right)\ne \mathrm{+\infty }$$
Assertion	limsupubuzmpt	$$⊢\phi \to \exists x\in ℝ\forall j\in ZB\le x$$

Proof

Step	Hyp	Ref	Expression
1		limsupubuzmpt.j	$$⊢Ⅎj\phi$$
2		limsupubuzmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		limsupubuzmpt.b	$$⊢\left(\phi \wedge j\in Z\right)\to B\in ℝ$$
4		limsupubuzmpt.n	$$⊢\phi \to \mathrm{lim\; sup}\left(\left(j\in Z⟼B\right)\right)\ne \mathrm{+\infty }$$
5		nfmpt1	$$⊢\underset{\_}{Ⅎ}j\left(j\in Z⟼B\right)$$
6		eqid	$$⊢\left(j\in Z⟼B\right)=\left(j\in Z⟼B\right)$$
7	1 3 6	fmptdf	$$⊢\phi \to \left(j\in Z⟼B\right):Z⟶ℝ$$
8	5 2 7 4	limsupubuz	$$⊢\phi \to \exists y\in ℝ\forall j\in Z\left(j\in Z⟼B\right)\left(j\right)\le y$$
9	6	a1i	$$⊢\phi \to \left(j\in Z⟼B\right)=\left(j\in Z⟼B\right)$$
10	9 3	fvmpt2d	$$⊢\left(\phi \wedge j\in Z\right)\to \left(j\in Z⟼B\right)\left(j\right)=B$$
11	10	breq1d	$$⊢\left(\phi \wedge j\in Z\right)\to \left(\left(j\in Z⟼B\right)\left(j\right)\le y\leftrightarrow B\le y\right)$$
12	1 11	ralbida	$$⊢\phi \to \left(\forall j\in Z\left(j\in Z⟼B\right)\left(j\right)\le y\leftrightarrow \forall j\in ZB\le y\right)$$
13	12	rexbidv	$$⊢\phi \to \left(\exists y\in ℝ\forall j\in Z\left(j\in Z⟼B\right)\left(j\right)\le y\leftrightarrow \exists y\in ℝ\forall j\in ZB\le y\right)$$
14	8 13	mpbid	$$⊢\phi \to \exists y\in ℝ\forall j\in ZB\le y$$
15		breq2	$$⊢y=x\to \left(B\le y\leftrightarrow B\le x\right)$$
16	15	ralbidv	$$⊢y=x\to \left(\forall j\in ZB\le y\leftrightarrow \forall j\in ZB\le x\right)$$
17	16	cbvrexvw	$$⊢\exists y\in ℝ\forall j\in ZB\le y\leftrightarrow \exists x\in ℝ\forall j\in ZB\le x$$
18	14 17	sylib	$$⊢\phi \to \exists x\in ℝ\forall j\in ZB\le x$$