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	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupbnd1f.2	$$⊢\phi \to B\subseteq ℝ$$
	limsupbnd1f.3	$$⊢\phi \to F:B⟶{ℝ}^{*}$$
	limsupbnd1f.4	$$⊢\phi \to A\in {ℝ}^{*}$$
	limsupbnd1f.5	$$⊢\phi \to \exists k\in ℝ\forall j\in B\left(k\le j\to F\left(j\right)\le A\right)$$
Assertion	limsupbnd1f	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\le A$$

Proof

Step	Hyp	Ref	Expression
1		limsupbnd1f.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupbnd1f.2	$$⊢\phi \to B\subseteq ℝ$$
3		limsupbnd1f.3	$$⊢\phi \to F:B⟶{ℝ}^{*}$$
4		limsupbnd1f.4	$$⊢\phi \to A\in {ℝ}^{*}$$
5		limsupbnd1f.5	$$⊢\phi \to \exists k\in ℝ\forall j\in B\left(k\le j\to F\left(j\right)\le A\right)$$
6		breq1	$$⊢k=i\to \left(k\le j\leftrightarrow i\le j\right)$$
7	6	imbi1d	$$⊢k=i\to \left(\left(k\le j\to F\left(j\right)\le A\right)\leftrightarrow \left(i\le j\to F\left(j\right)\le A\right)\right)$$
8	7	ralbidv	$$⊢k=i\to \left(\forall j\in B\left(k\le j\to F\left(j\right)\le A\right)\leftrightarrow \forall j\in B\left(i\le j\to F\left(j\right)\le A\right)\right)$$
9		nfv	$$⊢Ⅎl\left(i\le j\to F\left(j\right)\le A\right)$$
10		nfv	$$⊢Ⅎji\le l$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
12	1 11	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}jA$$
15	12 13 14	nfbr	$$⊢ℲjF\left(l\right)\le A$$
16	10 15	nfim	$$⊢Ⅎj\left(i\le l\to F\left(l\right)\le A\right)$$
17		breq2	$$⊢j=l\to \left(i\le j\leftrightarrow i\le l\right)$$
18		fveq2	$$⊢j=l\to F\left(j\right)=F\left(l\right)$$
19	18	breq1d	$$⊢j=l\to \left(F\left(j\right)\le A\leftrightarrow F\left(l\right)\le A\right)$$
20	17 19	imbi12d	$$⊢j=l\to \left(\left(i\le j\to F\left(j\right)\le A\right)\leftrightarrow \left(i\le l\to F\left(l\right)\le A\right)\right)$$
21	9 16 20	cbvralw	$$⊢\forall j\in B\left(i\le j\to F\left(j\right)\le A\right)\leftrightarrow \forall l\in B\left(i\le l\to F\left(l\right)\le A\right)$$
22	21	a1i	$$⊢k=i\to \left(\forall j\in B\left(i\le j\to F\left(j\right)\le A\right)\leftrightarrow \forall l\in B\left(i\le l\to F\left(l\right)\le A\right)\right)$$
23	8 22	bitrd	$$⊢k=i\to \left(\forall j\in B\left(k\le j\to F\left(j\right)\le A\right)\leftrightarrow \forall l\in B\left(i\le l\to F\left(l\right)\le A\right)\right)$$
24	23	cbvrexvw	$$⊢\exists k\in ℝ\forall j\in B\left(k\le j\to F\left(j\right)\le A\right)\leftrightarrow \exists i\in ℝ\forall l\in B\left(i\le l\to F\left(l\right)\le A\right)$$
25	5 24	sylib	$$⊢\phi \to \exists i\in ℝ\forall l\in B\left(i\le l\to F\left(l\right)\le A\right)$$
26	2 3 4 25	limsupbnd1	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\le A$$