Theorem psrbagf

Description: A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024)

	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	$$⊢F\in D\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	eleq2i	$$⊢F\in D\leftrightarrow F\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		elrabi	$$⊢F\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to F\in \left({{\mathbb{N}}_0}^I\right)$$
4		elmapi	$$⊢F\in \left({{\mathbb{N}}_0}^I\right)\to F:I⟶{\mathbb{N}}_0$$
5	3 4	syl	$$⊢F\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to F:I⟶{\mathbb{N}}_0$$
6	2 5	sylbi	$$⊢F\in D\to F:I⟶{\mathbb{N}}_0$$