Theorem psrbagres

Description: Restrict a bag of variables in I to a bag of variables in J C_ I . (Contributed by SN, 10-Mar-2025)

	Ref	Expression
Hypotheses	psrbagres.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrbagres.e	$$⊢E=\left\{g\in \left({{\mathbb{N}}_0}^J\right)|g^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrbagres.i	$$⊢\phi \to I\in V$$
	psrbagres.j	$$⊢\phi \to J\subseteq I$$
	psrbagres.f	$$⊢\phi \to F\in D$$
Assertion	psrbagres	$$⊢\phi \to {F\upharpoonright }_J\in E$$

Proof

Step	Hyp	Ref	Expression
1		psrbagres.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		psrbagres.e	$$⊢E=\left\{g\in \left({{\mathbb{N}}_0}^J\right)|g^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		psrbagres.i	$$⊢\phi \to I\in V$$
4		psrbagres.j	$$⊢\phi \to J\subseteq I$$
5		psrbagres.f	$$⊢\phi \to F\in D$$
6	1	psrbagf	$$⊢F\in D\to F:I⟶{\mathbb{N}}_0$$
7	5 6	syl	$$⊢\phi \to F:I⟶{\mathbb{N}}_0$$
8	7 4	fssresd	$$⊢\phi \to \left({F\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
9	1	psrbagfsupp	$$⊢F\in D\to {finSupp}_0\left(F\right)$$
10	5 9	syl	$$⊢\phi \to {finSupp}_0\left(F\right)$$
11		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
12	10 11	fsuppres	$$⊢\phi \to {finSupp}_0\left(\left({F\upharpoonright }_J\right)\right)$$
13	5	resexd	$$⊢\phi \to {F\upharpoonright }_J\in \mathrm{V}$$
14		fcdmnn0fsuppg	$$⊢\left({F\upharpoonright }_J\in \mathrm{V}\wedge \left({F\upharpoonright }_J\right):J⟶{\mathbb{N}}_0\right)\to \left({finSupp}_0\left(\left({F\upharpoonright }_J\right)\right)\leftrightarrow {\left({F\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
15	13 8 14	syl2anc	$$⊢\phi \to \left({finSupp}_0\left(\left({F\upharpoonright }_J\right)\right)\leftrightarrow {\left({F\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
16	12 15	mpbid	$$⊢\phi \to {\left({F\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
17	3 4	ssexd	$$⊢\phi \to J\in \mathrm{V}$$
18	2	psrbag	$$⊢J\in \mathrm{V}\to \left({F\upharpoonright }_J\in E\leftrightarrow \left(\left({F\upharpoonright }_J\right):J⟶{\mathbb{N}}_0\wedge {\left({F\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
19	17 18	syl	$$⊢\phi \to \left({F\upharpoonright }_J\in E\leftrightarrow \left(\left({F\upharpoonright }_J\right):J⟶{\mathbb{N}}_0\wedge {\left({F\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
20	8 16 19	mpbir2and	$$⊢\phi \to {F\upharpoonright }_J\in E$$