Theorem psrbag0

Description: The empty bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015)

	Ref	Expression
Hypothesis	psrbag0.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion	psrbag0	|- ( I e. V -> ( I X. { 0 } ) e. D )

Proof

Step	Hyp	Ref	Expression
1		psrbag0.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2		0nn0	|- 0 e. NN0
3	2	fconst6	|- ( I X. { 0 } ) : I --> NN0
4		c0ex	|- 0 e. _V
5	4	fconst	|- ( I X. { 0 } ) : I --> { 0 }
6		incom	|- ( { 0 } i^i NN ) = ( NN i^i { 0 } )
7		0nnn	|- -. 0 e. NN
8		disjsn	|- ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
9	7 8	mpbir	|- ( NN i^i { 0 } ) = (/)
10	6 9	eqtri	|- ( { 0 } i^i NN ) = (/)
11		fimacnvdisj	|- ( ( ( I X. { 0 } ) : I --> { 0 } /\ ( { 0 } i^i NN ) = (/) ) -> ( `' ( I X. { 0 } ) " NN ) = (/) )
12	5 10 11	mp2an	|- ( `' ( I X. { 0 } ) " NN ) = (/)
13		0fin	|- (/) e. Fin
14	12 13	eqeltri	|- ( `' ( I X. { 0 } ) " NN ) e. Fin
15	3 14	pm3.2i	|- ( ( I X. { 0 } ) : I --> NN0 /\ ( `' ( I X. { 0 } ) " NN ) e. Fin )
16	1	psrbag	|- ( I e. V -> ( ( I X. { 0 } ) e. D <-> ( ( I X. { 0 } ) : I --> NN0 /\ ( `' ( I X. { 0 } ) " NN ) e. Fin ) ) )
17	15 16	mpbiri	|- ( I e. V -> ( I X. { 0 } ) e. D )