Theorem psrbag0

Description: The empty bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		psrbag0.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	2	fconst6	$$⊢\left(I\times \left\{0\right\}\right):I⟶{\mathbb{N}}_0$$
4		c0ex	$$⊢0\in \mathrm{V}$$
5	4	fconst	$$⊢\left(I\times \left\{0\right\}\right):I⟶\left\{0\right\}$$
6		incom	$$⊢\left\{0\right\}\cap \mathbb{N}=\mathbb{N}\cap \left\{0\right\}$$
7		0nnn	$$⊢\neg 0\in \mathbb{N}$$
8		disjsn	$$⊢\mathbb{N}\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in \mathbb{N}$$
9	7 8	mpbir	$$⊢\mathbb{N}\cap \left\{0\right\}=\varnothing$$
10	6 9	eqtri	$$⊢\left\{0\right\}\cap \mathbb{N}=\varnothing$$
11		fimacnvdisj	$$⊢\left(\left(I\times \left\{0\right\}\right):I⟶\left\{0\right\}\wedge \left\{0\right\}\cap \mathbb{N}=\varnothing \right)\to {\left(I\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]=\varnothing$$
12	5 10 11	mp2an	$$⊢{\left(I\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]=\varnothing$$
13		0fi	$$⊢\varnothing \in \mathrm{Fin}$$
14	12 13	eqeltri	$$⊢{\left(I\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
15	3 14	pm3.2i	$$⊢\left(\left(I\times \left\{0\right\}\right):I⟶{\mathbb{N}}_0\wedge {\left(I\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
16	1	psrbag	$$⊢I\in V\to \left(I\times \left\{0\right\}\in D\leftrightarrow \left(\left(I\times \left\{0\right\}\right):I⟶{\mathbb{N}}_0\wedge {\left(I\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
17	15 16	mpbiri	$$⊢I\in V\to I\times \left\{0\right\}\in D$$