Theorem psrbag

Description: Elementhood in the set of finite bags. (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	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)$$

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		cnveq	$$⊢f=F\to f^{-1}=F^{-1}$$
3	2	imaeq1d	$$⊢f=F\to f^{-1}\left[\mathbb{N}\right]=F^{-1}\left[\mathbb{N}\right]$$
4	3	eleq1d	$$⊢f=F\to \left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
5	4 1	elrab2	$$⊢F\in D\leftrightarrow \left(F\in \left({{\mathbb{N}}_0}^I\right)\wedge F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
6		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
7		elmapg	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge I\in V\right)\to \left(F\in \left({{\mathbb{N}}_0}^I\right)\leftrightarrow F:I⟶{\mathbb{N}}_0\right)$$
8	6 7	mpan	$$⊢I\in V\to \left(F\in \left({{\mathbb{N}}_0}^I\right)\leftrightarrow F:I⟶{\mathbb{N}}_0\right)$$
9	8	anbi1d	$$⊢I\in V\to \left(\left(F\in \left({{\mathbb{N}}_0}^I\right)\wedge F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\leftrightarrow \left(F:I⟶{\mathbb{N}}_0\wedge F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
10	5 9	bitrid	$$⊢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)$$