Theorem liminflelimsup

Description: The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex for a counterexample). The inequality can be strict, see liminfltlimsupex . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminflelimsup.1	$$⊢\phi \to F\in V$$
	liminflelimsup.2	$$⊢\phi \to \forall k\in ℝ\exists j\in \left[k,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing$$
Assertion	liminflelimsup	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)\le \mathrm{lim\; sup}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		liminflelimsup.1	$$⊢\phi \to F\in V$$
2		liminflelimsup.2	$$⊢\phi \to \forall k\in ℝ\exists j\in \left[k,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing$$
3		oveq1	$$⊢k=i\to \left[k,\mathrm{+\infty }\right)=\left[i,\mathrm{+\infty }\right)$$
4	3	rexeqdv	$$⊢k=i\to \left(\exists j\in \left[k,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \leftrightarrow \exists j\in \left[i,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$$
5		oveq1	$$⊢j=l\to \left[j,\mathrm{+\infty }\right)=\left[l,\mathrm{+\infty }\right)$$
6	5	imaeq2d	$$⊢j=l\to F\left[\left[j,\mathrm{+\infty }\right)\right]=F\left[\left[l,\mathrm{+\infty }\right)\right]$$
7	6	ineq1d	$$⊢j=l\to F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=F\left[\left[l,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}$$
8	7	neeq1d	$$⊢j=l\to \left(F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \leftrightarrow F\left[\left[l,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$$
9	8	cbvrexvw	$$⊢\exists j\in \left[i,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \leftrightarrow \exists l\in \left[i,\mathrm{+\infty }\right)F\left[\left[l,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing$$
10	9	a1i	$$⊢k=i\to \left(\exists j\in \left[i,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \leftrightarrow \exists l\in \left[i,\mathrm{+\infty }\right)F\left[\left[l,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$$
11	4 10	bitrd	$$⊢k=i\to \left(\exists j\in \left[k,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \leftrightarrow \exists l\in \left[i,\mathrm{+\infty }\right)F\left[\left[l,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$$
12	11	cbvralvw	$$⊢\forall k\in ℝ\exists j\in \left[k,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \leftrightarrow \forall i\in ℝ\exists l\in \left[i,\mathrm{+\infty }\right)F\left[\left[l,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing$$
13	2 12	sylib	$$⊢\phi \to \forall i\in ℝ\exists l\in \left[i,\mathrm{+\infty }\right)F\left[\left[l,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing$$
14	1 13	liminflelimsuplem	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)\le \mathrm{lim\; sup}\left(F\right)$$