Theorem psrbagsn

Description: A singleton 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	psrbagsn	$$⊢I\in V\to \left(x\in I⟼if\left(x=K,1,0\right)\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		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	2 3	ifcli	$$⊢if\left(x=K,1,0\right)\in {\mathbb{N}}_0$$
5	4	a1i	$$⊢\left(\top \wedge x\in I\right)\to if\left(x=K,1,0\right)\in {\mathbb{N}}_0$$
6	5	fmpttd	$$⊢\top \to \left(x\in I⟼if\left(x=K,1,0\right)\right):I⟶{\mathbb{N}}_0$$
7	6	mptru	$$⊢\left(x\in I⟼if\left(x=K,1,0\right)\right):I⟶{\mathbb{N}}_0$$
8		eqid	$$⊢\left(x\in I⟼if\left(x=K,1,0\right)\right)=\left(x\in I⟼if\left(x=K,1,0\right)\right)$$
9	8	mptpreima	$$⊢{\left(x\in I⟼if\left(x=K,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]=\left\{x\in I|if\left(x=K,1,0\right)\in \mathbb{N}\right\}$$
10		snfi	$$⊢\left\{K\right\}\in \mathrm{Fin}$$
11		inss1	$$⊢\left\{x|x=K\right\}\cap I\subseteq \left\{x|x=K\right\}$$
12		dfrab2	$$⊢\left\{x\in I|x=K\right\}=\left\{x|x=K\right\}\cap I$$
13		df-sn	$$⊢\left\{K\right\}=\left\{x|x=K\right\}$$
14	11 12 13	3sstr4i	$$⊢\left\{x\in I|x=K\right\}\subseteq \left\{K\right\}$$
15		ssfi	$$⊢\left(\left\{K\right\}\in \mathrm{Fin}\wedge \left\{x\in I|x=K\right\}\subseteq \left\{K\right\}\right)\to \left\{x\in I|x=K\right\}\in \mathrm{Fin}$$
16	10 14 15	mp2an	$$⊢\left\{x\in I|x=K\right\}\in \mathrm{Fin}$$
17		0nnn	$$⊢\neg 0\in \mathbb{N}$$
18		iffalse	$$⊢\neg x=K\to if\left(x=K,1,0\right)=0$$
19	18	eleq1d	$$⊢\neg x=K\to \left(if\left(x=K,1,0\right)\in \mathbb{N}\leftrightarrow 0\in \mathbb{N}\right)$$
20	17 19	mtbiri	$$⊢\neg x=K\to \neg if\left(x=K,1,0\right)\in \mathbb{N}$$
21	20	con4i	$$⊢if\left(x=K,1,0\right)\in \mathbb{N}\to x=K$$
22	21	a1i	$$⊢x\in I\to \left(if\left(x=K,1,0\right)\in \mathbb{N}\to x=K\right)$$
23	22	ss2rabi	$$⊢\left\{x\in I|if\left(x=K,1,0\right)\in \mathbb{N}\right\}\subseteq \left\{x\in I|x=K\right\}$$
24		ssfi	$$⊢\left(\left\{x\in I|x=K\right\}\in \mathrm{Fin}\wedge \left\{x\in I|if\left(x=K,1,0\right)\in \mathbb{N}\right\}\subseteq \left\{x\in I|x=K\right\}\right)\to \left\{x\in I|if\left(x=K,1,0\right)\in \mathbb{N}\right\}\in \mathrm{Fin}$$
25	16 23 24	mp2an	$$⊢\left\{x\in I|if\left(x=K,1,0\right)\in \mathbb{N}\right\}\in \mathrm{Fin}$$
26	9 25	eqeltri	$$⊢{\left(x\in I⟼if\left(x=K,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
27	7 26	pm3.2i	$$⊢\left(\left(x\in I⟼if\left(x=K,1,0\right)\right):I⟶{\mathbb{N}}_0\wedge {\left(x\in I⟼if\left(x=K,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
28	1	psrbag	$$⊢I\in V\to \left(\left(x\in I⟼if\left(x=K,1,0\right)\right)\in D\leftrightarrow \left(\left(x\in I⟼if\left(x=K,1,0\right)\right):I⟶{\mathbb{N}}_0\wedge {\left(x\in I⟼if\left(x=K,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
29	27 28	mpbiri	$$⊢I\in V\to \left(x\in I⟼if\left(x=K,1,0\right)\right)\in D$$