Theorem psrbagf

Description: A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014)

	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	psrbagf	$$⊢\left(I\in V\wedge F\in D\right)\to F:I⟶{\mathbb{N}}_0$$

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	1	psrbag	$$⊢I\in V\to \left(F\in D\leftrightarrow \left(F:I⟶{\mathbb{N}}_0\wedge F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
3	2	simprbda	$$⊢\left(I\in V\wedge F\in D\right)\to F:I⟶{\mathbb{N}}_0$$