This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( NN0 ^m 1o ) = { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin }

Proof

Step Hyp Ref Expression
1 rabid2 
 |-  ( ( NN0 ^m 1o ) = { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin } <-> A. f e. ( NN0 ^m 1o ) ( `' f " NN ) e. Fin )
2 df1o2 
 |-  1o = { (/) }
3 snfi 
 |-  { (/) } e. Fin
4 2 3 eqeltri 
 |-  1o e. Fin
5 cnvimass 
 |-  ( `' f " NN ) C_ dom f
6 elmapi 
 |-  ( f e. ( NN0 ^m 1o ) -> f : 1o --> NN0 )
7 5 6 fssdm 
 |-  ( f e. ( NN0 ^m 1o ) -> ( `' f " NN ) C_ 1o )
8 ssfi 
 |-  ( ( 1o e. Fin /\ ( `' f " NN ) C_ 1o ) -> ( `' f " NN ) e. Fin )
9 4 7 8 sylancr 
 |-  ( f e. ( NN0 ^m 1o ) -> ( `' f " NN ) e. Fin )
10 1 9 mprgbir 
 |-  ( NN0 ^m 1o ) = { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin }