Theorem psr1baslem

Description: The set of finite bags on 1o is just the set of all functions from 1o to NN0 . (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Assertion	psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rabid2	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\leftrightarrow \forall f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
2		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
3		snfi	$$⊢\left\{\varnothing \right\}\in \mathrm{Fin}$$
4	2 3	eqeltri	$$⊢1_{𝑜}\in \mathrm{Fin}$$
5		cnvimass	$$⊢f^{-1}\left[\mathbb{N}\right]\subseteq \mathrm{dom}f$$
6		elmapi	$$⊢f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to f:1_{𝑜}⟶{\mathbb{N}}_0$$
7	5 6	fssdm	$$⊢f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to f^{-1}\left[\mathbb{N}\right]\subseteq 1_{𝑜}$$
8		ssfi	$$⊢\left(1_{𝑜}\in \mathrm{Fin}\wedge f^{-1}\left[\mathbb{N}\right]\subseteq 1_{𝑜}\right)\to f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
9	4 7 8	sylancr	$$⊢f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
10	1 9	mprgbir	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$