Theorem psrbasfsupp

Description: Rewrite a finite support for nonnegative integers : For functions mapping a set I to the nonnegative integers, having finite support can also be written as having a finite preimage of the positive integers. The latter expression is used for example in psrbas , but with the former expression, theorems about finite support can be used more directly. (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypothesis	psrbasfsupp.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(f\right)\right\}$$
Assertion	psrbasfsupp	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		psrbasfsupp.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(f\right)\right\}$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3		isfsupp	$$⊢\left(f\in \left({{\mathbb{N}}_0}^I\right)\wedge 0\in {\mathbb{N}}_0\right)\to \left({finSupp}_0\left(f\right)\leftrightarrow \left(\mathrm{Fun}f\wedge f\mathrm{supp}0\in \mathrm{Fin}\right)\right)$$
4	2 3	mpan2	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \left({finSupp}_0\left(f\right)\leftrightarrow \left(\mathrm{Fun}f\wedge f\mathrm{supp}0\in \mathrm{Fin}\right)\right)$$
5		elmapfun	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \mathrm{Fun}f$$
6	5	biantrurd	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \left(f\mathrm{supp}0\in \mathrm{Fin}\leftrightarrow \left(\mathrm{Fun}f\wedge f\mathrm{supp}0\in \mathrm{Fin}\right)\right)$$
7		dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$
8	7	ineq2i	$$⊢\mathrm{ran}f\cap \mathbb{N}=\mathrm{ran}f\cap \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)$$
9		incom	$$⊢\mathrm{ran}f\cap \mathbb{N}=\mathbb{N}\cap \mathrm{ran}f$$
10		indif2	$$⊢\mathrm{ran}f\cap \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)=\left(\mathrm{ran}f\cap {\mathbb{N}}_0\right)\setminus \left\{0\right\}$$
11	8 9 10	3eqtr3i	$$⊢\mathbb{N}\cap \mathrm{ran}f=\left(\mathrm{ran}f\cap {\mathbb{N}}_0\right)\setminus \left\{0\right\}$$
12		elmapi	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to f:I⟶{\mathbb{N}}_0$$
13	12	frnd	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \mathrm{ran}f\subseteq {\mathbb{N}}_0$$
14		dfss2	$$⊢\mathrm{ran}f\subseteq {\mathbb{N}}_0\leftrightarrow \mathrm{ran}f\cap {\mathbb{N}}_0=\mathrm{ran}f$$
15	13 14	sylib	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \mathrm{ran}f\cap {\mathbb{N}}_0=\mathrm{ran}f$$
16	15	difeq1d	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \left(\mathrm{ran}f\cap {\mathbb{N}}_0\right)\setminus \left\{0\right\}=\mathrm{ran}f\setminus \left\{0\right\}$$
17	11 16	eqtrid	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \mathbb{N}\cap \mathrm{ran}f=\mathrm{ran}f\setminus \left\{0\right\}$$
18	17	imaeq2d	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to f^{-1}\left[\mathbb{N}\cap \mathrm{ran}f\right]=f^{-1}\left[\mathrm{ran}f\setminus \left\{0\right\}\right]$$
19		fimacnvinrn	$$⊢\mathrm{Fun}f\to f^{-1}\left[\mathbb{N}\right]=f^{-1}\left[\mathbb{N}\cap \mathrm{ran}f\right]$$
20	5 19	syl	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to f^{-1}\left[\mathbb{N}\right]=f^{-1}\left[\mathbb{N}\cap \mathrm{ran}f\right]$$
21		id	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to f\in \left({{\mathbb{N}}_0}^I\right)$$
22	2	a1i	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to 0\in {\mathbb{N}}_0$$
23		supppreima	$$⊢\left(\mathrm{Fun}f\wedge f\in \left({{\mathbb{N}}_0}^I\right)\wedge 0\in {\mathbb{N}}_0\right)\to f\mathrm{supp}0=f^{-1}\left[\mathrm{ran}f\setminus \left\{0\right\}\right]$$
24	5 21 22 23	syl3anc	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to f\mathrm{supp}0=f^{-1}\left[\mathrm{ran}f\setminus \left\{0\right\}\right]$$
25	18 20 24	3eqtr4rd	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to f\mathrm{supp}0=f^{-1}\left[\mathbb{N}\right]$$
26	25	eleq1d	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \left(f\mathrm{supp}0\in \mathrm{Fin}\leftrightarrow f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
27	4 6 26	3bitr2d	$$⊢f\in \left({{\mathbb{N}}_0}^I\right)\to \left({finSupp}_0\left(f\right)\leftrightarrow f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
28	27	rabbiia	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(f\right)\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
29	1 28	eqtri	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$