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

Proof

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