Theorem psrbagfsupp

Description: Finite bags have finite nonzero-support. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 18-Jul-2019)

	Ref	Expression
Hypothesis	psrbagfsupp.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
Assertion	psrbagfsupp	$$⊢\left(X\in D\wedge I\in V\right)\to {finSupp}_0\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		psrbagfsupp.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2	1	psrbag	$$⊢I\in V\to \left(X\in D\leftrightarrow \left(X:I⟶{\mathbb{N}}_0\wedge X^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
3	2	biimpac	$$⊢\left(X\in D\wedge I\in V\right)\to \left(X:I⟶{\mathbb{N}}_0\wedge X^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
4	3	simprd	$$⊢\left(X\in D\wedge I\in V\right)\to X^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
5		simpr	$$⊢\left(X\in D\wedge I\in V\right)\to I\in V$$
6	1	psrbagf	$$⊢\left(I\in V\wedge X\in D\right)\to X:I⟶{\mathbb{N}}_0$$
7	6	ancoms	$$⊢\left(X\in D\wedge I\in V\right)\to X:I⟶{\mathbb{N}}_0$$
8		frnnn0fsupp	$$⊢\left(I\in V\wedge X:I⟶{\mathbb{N}}_0\right)\to \left({finSupp}_0\left(X\right)\leftrightarrow X^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
9	5 7 8	syl2anc	$$⊢\left(X\in D\wedge I\in V\right)\to \left({finSupp}_0\left(X\right)\leftrightarrow X^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
10	4 9	mpbird	$$⊢\left(X\in D\wedge I\in V\right)\to {finSupp}_0\left(X\right)$$