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 }