Theorem limsuppnfd

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsuppnfd.j	$$⊢\underset{\_}{Ⅎ}jF$$
	limsuppnfd.a	$$⊢\phi \to A\subseteq ℝ$$
	limsuppnfd.f	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
	limsuppnfd.u	$$⊢\phi \to \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
Assertion	limsuppnfd	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		limsuppnfd.j	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsuppnfd.a	$$⊢\phi \to A\subseteq ℝ$$
3		limsuppnfd.f	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
4		limsuppnfd.u	$$⊢\phi \to \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
5		breq1	$$⊢x=y\to \left(x\le F\left(j\right)\leftrightarrow y\le F\left(j\right)\right)$$
6	5	anbi2d	$$⊢x=y\to \left(\left(k\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \left(k\le j\wedge y\le F\left(j\right)\right)\right)$$
7	6	rexbidv	$$⊢x=y\to \left(\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)\right)$$
8		breq1	$$⊢k=i\to \left(k\le j\leftrightarrow i\le j\right)$$
9	8	anbi1d	$$⊢k=i\to \left(\left(k\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \left(i\le j\wedge y\le F\left(j\right)\right)\right)$$
10	9	rexbidv	$$⊢k=i\to \left(\exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \exists j\in A\left(i\le j\wedge y\le F\left(j\right)\right)\right)$$
11		nfv	$$⊢Ⅎl\left(i\le j\wedge y\le F\left(j\right)\right)$$
12		nfv	$$⊢Ⅎji\le l$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}jy$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
16	1 15	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
17	13 14 16	nfbr	$$⊢Ⅎjy\le F\left(l\right)$$
18	12 17	nfan	$$⊢Ⅎj\left(i\le l\wedge y\le F\left(l\right)\right)$$
19		breq2	$$⊢j=l\to \left(i\le j\leftrightarrow i\le l\right)$$
20		fveq2	$$⊢j=l\to F\left(j\right)=F\left(l\right)$$
21	20	breq2d	$$⊢j=l\to \left(y\le F\left(j\right)\leftrightarrow y\le F\left(l\right)\right)$$
22	19 21	anbi12d	$$⊢j=l\to \left(\left(i\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \left(i\le l\wedge y\le F\left(l\right)\right)\right)$$
23	11 18 22	cbvrexw	$$⊢\exists j\in A\left(i\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)$$
24	23	a1i	$$⊢k=i\to \left(\exists j\in A\left(i\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\right)$$
25	10 24	bitrd	$$⊢k=i\to \left(\exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\right)$$
26	7 25	cbvral2vw	$$⊢\forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \forall y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)$$
27	4 26	sylib	$$⊢\phi \to \forall y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)$$
28		eqid	$$⊢\left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
29	2 3 27 28	limsuppnfdlem	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=\mathrm{+\infty }$$