Theorem liminfcl

Description: Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	liminfcl	$$⊢F\in V\to \mathrm{lim\; inf}\left(F\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(k\in ℝ⟼inf\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left(k\in ℝ⟼inf\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
2	1	liminfval	$$⊢F\in V\to \mathrm{lim\; inf}\left(F\right)=sup\left(\mathrm{ran}\left(k\in ℝ⟼inf\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$$
3		nfv	$$⊢ℲkF\in V$$
4		inss2	$$⊢F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\subseteq {ℝ}^{*}$$
5		infxrcl	$$⊢F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\subseteq {ℝ}^{*}\to inf\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
6	4 5	ax-mp	$$⊢inf\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
7	6	a1i	$$⊢\left(F\in V\wedge k\in ℝ\right)\to inf\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
8	3 1 7	rnmptssd	$$⊢F\in V\to \mathrm{ran}\left(k\in ℝ⟼inf\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)\subseteq {ℝ}^{*}$$
9	8	supxrcld	$$⊢F\in V\to sup\left(\mathrm{ran}\left(k\in ℝ⟼inf\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$$
10	2 9	eqeltrd	$$⊢F\in V\to \mathrm{lim\; inf}\left(F\right)\in {ℝ}^{*}$$