Theorem snifpsrbag

Description: A bag containing one element is a finite bag. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by AV, 8-Jul-2019)

	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	snifpsrbag	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(y\in I⟼if\left(y=X,N,0\right)\right)\in D$$

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		simpr	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	3	a1i	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to 0\in {\mathbb{N}}_0$$
5	2 4	ifcld	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to if\left(y=X,N,0\right)\in {\mathbb{N}}_0$$
6	5	adantr	$$⊢\left(\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\wedge y\in I\right)\to if\left(y=X,N,0\right)\in {\mathbb{N}}_0$$
7	6	fmpttd	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(y\in I⟼if\left(y=X,N,0\right)\right):I⟶{\mathbb{N}}_0$$
8		id	$$⊢I\in V\to I\in V$$
9		c0ex	$$⊢0\in \mathrm{V}$$
10	9	a1i	$$⊢I\in V\to 0\in \mathrm{V}$$
11		eqid	$$⊢\left(y\in I⟼if\left(y=X,N,0\right)\right)=\left(y\in I⟼if\left(y=X,N,0\right)\right)$$
12	8 10 11	sniffsupp	$$⊢I\in V\to {finSupp}_0\left(\left(y\in I⟼if\left(y=X,N,0\right)\right)\right)$$
13	12	adantr	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to {finSupp}_0\left(\left(y\in I⟼if\left(y=X,N,0\right)\right)\right)$$
14		frnnn0fsupp	$$⊢\left(I\in V\wedge \left(y\in I⟼if\left(y=X,N,0\right)\right):I⟶{\mathbb{N}}_0\right)\to \left({finSupp}_0\left(\left(y\in I⟼if\left(y=X,N,0\right)\right)\right)\leftrightarrow {\left(y\in I⟼if\left(y=X,N,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
15	14	adantlr	$$⊢\left(\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\wedge \left(y\in I⟼if\left(y=X,N,0\right)\right):I⟶{\mathbb{N}}_0\right)\to \left({finSupp}_0\left(\left(y\in I⟼if\left(y=X,N,0\right)\right)\right)\leftrightarrow {\left(y\in I⟼if\left(y=X,N,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
16	15	bicomd	$$⊢\left(\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\wedge \left(y\in I⟼if\left(y=X,N,0\right)\right):I⟶{\mathbb{N}}_0\right)\to \left({\left(y\in I⟼if\left(y=X,N,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow {finSupp}_0\left(\left(y\in I⟼if\left(y=X,N,0\right)\right)\right)\right)$$
17	7 16	mpdan	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to \left({\left(y\in I⟼if\left(y=X,N,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow {finSupp}_0\left(\left(y\in I⟼if\left(y=X,N,0\right)\right)\right)\right)$$
18	13 17	mpbird	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to {\left(y\in I⟼if\left(y=X,N,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
19	1	psrbag	$$⊢I\in V\to \left(\left(y\in I⟼if\left(y=X,N,0\right)\right)\in D\leftrightarrow \left(\left(y\in I⟼if\left(y=X,N,0\right)\right):I⟶{\mathbb{N}}_0\wedge {\left(y\in I⟼if\left(y=X,N,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
20	19	adantr	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(\left(y\in I⟼if\left(y=X,N,0\right)\right)\in D\leftrightarrow \left(\left(y\in I⟼if\left(y=X,N,0\right)\right):I⟶{\mathbb{N}}_0\wedge {\left(y\in I⟼if\left(y=X,N,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
21	7 18 20	mpbir2and	$$⊢\left(I\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(y\in I⟼if\left(y=X,N,0\right)\right)\in D$$