Theorem liminfresuz2

Description: If the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfresuz2.1	$$⊢\phi \to M\in \mathbb{Z}$$
	liminfresuz2.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	liminfresuz2.3	$$⊢\phi \to F\in V$$
	liminfresuz2.4	$$⊢\phi \to \mathrm{dom}F\subseteq \mathbb{Z}$$
Assertion	liminfresuz2	$$⊢\phi \to \mathrm{lim\; inf}\left({F\upharpoonright }_Z\right)=\mathrm{lim\; inf}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		liminfresuz2.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		liminfresuz2.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		liminfresuz2.3	$$⊢\phi \to F\in V$$
4		liminfresuz2.4	$$⊢\phi \to \mathrm{dom}F\subseteq \mathbb{Z}$$
5		dmresss	$$⊢\mathrm{dom}\left({F\upharpoonright }_{ℝ}\right)\subseteq \mathrm{dom}F$$
6	5	a1i	$$⊢\phi \to \mathrm{dom}\left({F\upharpoonright }_{ℝ}\right)\subseteq \mathrm{dom}F$$
7	6 4	sstrd	$$⊢\phi \to \mathrm{dom}\left({F\upharpoonright }_{ℝ}\right)\subseteq \mathbb{Z}$$
8	1 2 3 7	liminfresuz	$$⊢\phi \to \mathrm{lim\; inf}\left({F\upharpoonright }_Z\right)=\mathrm{lim\; inf}\left(F\right)$$