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 01𝑜=f01𝑜|f-1Fin

Proof

Step Hyp Ref Expression
1 rabid2 01𝑜=f01𝑜|f-1Finf01𝑜f-1Fin
2 df1o2 1𝑜=
3 snfi Fin
4 2 3 eqeltri 1𝑜Fin
5 cnvimass f-1domf
6 elmapi f01𝑜f:1𝑜0
7 5 6 fssdm f01𝑜f-11𝑜
8 ssfi 1𝑜Finf-11𝑜f-1Fin
9 4 7 8 sylancr f01𝑜f-1Fin
10 1 9 mprgbir 01𝑜=f01𝑜|f-1Fin