Theorem fczpsrbag

Description: The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019)

	Ref	Expression
Hypothesis	psrbag.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
Assertion	fczpsrbag	$$⊢I\in V\to \left(x\in I⟼0\right)\in D$$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		ifid	$$⊢if\left(x=n,0,0\right)=0$$
3	2	eqcomi	$$⊢0=if\left(x=n,0,0\right)$$
4	3	a1i	$$⊢I\in V\to 0=if\left(x=n,0,0\right)$$
5	4	mpteq2dv	$$⊢I\in V\to \left(x\in I⟼0\right)=\left(x\in I⟼if\left(x=n,0,0\right)\right)$$
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7	1	snifpsrbag	$$⊢\left(I\in V\wedge 0\in {\mathbb{N}}_0\right)\to \left(x\in I⟼if\left(x=n,0,0\right)\right)\in D$$
8	6 7	mpan2	$$⊢I\in V\to \left(x\in I⟼if\left(x=n,0,0\right)\right)\in D$$
9	5 8	eqeltrd	$$⊢I\in V\to \left(x\in I⟼0\right)\in D$$