Theorem limsupmnf

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		limsupmnf.j	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupmnf.a	$$⊢\phi \to A\subseteq ℝ$$
3		limsupmnf.f	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
4		eqid	$$⊢\left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)$$
5	2 3 4	limsupmnflem	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\leftrightarrow \forall y\in ℝ\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)\le y\right)\right)$$
6		breq2	$$⊢y=x\to \left(F\left(l\right)\le y\leftrightarrow F\left(l\right)\le x\right)$$
7	6	imbi2d	$$⊢y=x\to \left(\left(i\le l\to F\left(l\right)\le y\right)\leftrightarrow \left(i\le l\to F\left(l\right)\le x\right)\right)$$
8	7	ralbidv	$$⊢y=x\to \left(\forall l\in A\left(i\le l\to F\left(l\right)\le y\right)\leftrightarrow \forall l\in A\left(i\le l\to F\left(l\right)\le x\right)\right)$$
9	8	rexbidv	$$⊢y=x\to \left(\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)\le y\right)\leftrightarrow \exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)\le x\right)\right)$$
10		breq1	$$⊢i=k\to \left(i\le l\leftrightarrow k\le l\right)$$
11	10	imbi1d	$$⊢i=k\to \left(\left(i\le l\to F\left(l\right)\le x\right)\leftrightarrow \left(k\le l\to F\left(l\right)\le x\right)\right)$$
12	11	ralbidv	$$⊢i=k\to \left(\forall l\in A\left(i\le l\to F\left(l\right)\le x\right)\leftrightarrow \forall l\in A\left(k\le l\to F\left(l\right)\le x\right)\right)$$
13		nfv	$$⊢Ⅎjk\le l$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
15	1 14	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}jx$$
18	15 16 17	nfbr	$$⊢ℲjF\left(l\right)\le x$$
19	13 18	nfim	$$⊢Ⅎj\left(k\le l\to F\left(l\right)\le x\right)$$
20		nfv	$$⊢Ⅎl\left(k\le j\to F\left(j\right)\le x\right)$$
21		breq2	$$⊢l=j\to \left(k\le l\leftrightarrow k\le j\right)$$
22		fveq2	$$⊢l=j\to F\left(l\right)=F\left(j\right)$$
23	22	breq1d	$$⊢l=j\to \left(F\left(l\right)\le x\leftrightarrow F\left(j\right)\le x\right)$$
24	21 23	imbi12d	$$⊢l=j\to \left(\left(k\le l\to F\left(l\right)\le x\right)\leftrightarrow \left(k\le j\to F\left(j\right)\le x\right)\right)$$
25	19 20 24	cbvralw	$$⊢\forall l\in A\left(k\le l\to F\left(l\right)\le x\right)\leftrightarrow \forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
26	25	a1i	$$⊢i=k\to \left(\forall l\in A\left(k\le l\to F\left(l\right)\le x\right)\leftrightarrow \forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\right)$$
27	12 26	bitrd	$$⊢i=k\to \left(\forall l\in A\left(i\le l\to F\left(l\right)\le x\right)\leftrightarrow \forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\right)$$
28	27	cbvrexvw	$$⊢\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)\le x\right)\leftrightarrow \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
29	28	a1i	$$⊢y=x\to \left(\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)\le x\right)\leftrightarrow \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\right)$$
30	9 29	bitrd	$$⊢y=x\to \left(\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)\le y\right)\leftrightarrow \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\right)$$
31	30	cbvralvw	$$⊢\forall y\in ℝ\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)\le y\right)\leftrightarrow \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
32	31	a1i	$$⊢\phi \to \left(\forall y\in ℝ\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)\le y\right)\leftrightarrow \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\right)$$
33	5 32	bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\right)$$