# Metamath Proof Explorer

## 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 ${⊢}{{ℕ}_{0}}^{{1}_{𝑜}}=\left\{{f}\in \left({{ℕ}_{0}}^{{1}_{𝑜}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$

### Proof

Step Hyp Ref Expression
1 rabid2 ${⊢}{{ℕ}_{0}}^{{1}_{𝑜}}=\left\{{f}\in \left({{ℕ}_{0}}^{{1}_{𝑜}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}↔\forall {f}\in \left({{ℕ}_{0}}^{{1}_{𝑜}}\right)\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[ℕ\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[ℕ\right]\subseteq \mathrm{dom}{f}$
6 elmapi ${⊢}{f}\in \left({{ℕ}_{0}}^{{1}_{𝑜}}\right)\to {f}:{1}_{𝑜}⟶{ℕ}_{0}$
7 5 6 fssdm ${⊢}{f}\in \left({{ℕ}_{0}}^{{1}_{𝑜}}\right)\to {{f}}^{-1}\left[ℕ\right]\subseteq {1}_{𝑜}$
8 ssfi ${⊢}\left({1}_{𝑜}\in \mathrm{Fin}\wedge {{f}}^{-1}\left[ℕ\right]\subseteq {1}_{𝑜}\right)\to {{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}$
9 4 7 8 sylancr ${⊢}{f}\in \left({{ℕ}_{0}}^{{1}_{𝑜}}\right)\to {{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}$
10 1 9 mprgbir ${⊢}{{ℕ}_{0}}^{{1}_{𝑜}}=\left\{{f}\in \left({{ℕ}_{0}}^{{1}_{𝑜}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$