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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabid2 | |
|
2 | df1o2 | |
|
3 | snfi | |
|
4 | 2 3 | eqeltri | |
5 | cnvimass | |
|
6 | elmapi | |
|
7 | 5 6 | fssdm | |
8 | ssfi | |
|
9 | 4 7 8 | sylancr | |
10 | 1 9 | mprgbir | |