Theorem limsupresuz2

Description: If the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		limsupresuz2.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		limsupresuz2.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		limsupresuz2.3	$$⊢\phi \to F\in V$$
4		limsupresuz2.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	limsupresuz	$$⊢\phi \to \mathrm{lim\; sup}\left({F\upharpoonright }_Z\right)=\mathrm{lim\; sup}\left(F\right)$$