Theorem psrbag

Description: Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypothesis	psrbag.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion	psrbag	|- ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2		cnveq	|- ( f = F -> `' f = `' F )
3	2	imaeq1d	|- ( f = F -> ( `' f " NN ) = ( `' F " NN ) )
4	3	eleq1d	|- ( f = F -> ( ( `' f " NN ) e. Fin <-> ( `' F " NN ) e. Fin ) )
5	4 1	elrab2	|- ( F e. D <-> ( F e. ( NN0 ^m I ) /\ ( `' F " NN ) e. Fin ) )
6		nn0ex	|- NN0 e. _V
7		elmapg	|- ( ( NN0 e. _V /\ I e. V ) -> ( F e. ( NN0 ^m I ) <-> F : I --> NN0 ) )
8	6 7	mpan	|- ( I e. V -> ( F e. ( NN0 ^m I ) <-> F : I --> NN0 ) )
9	8	anbi1d	|- ( I e. V -> ( ( F e. ( NN0 ^m I ) /\ ( `' F " NN ) e. Fin ) <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
10	5 9	bitrid	|- ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )