Theorem fczpsrbag

Description: The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2		ifid	|- if ( x = n , 0 , 0 ) = 0
3	2	eqcomi	|- 0 = if ( x = n , 0 , 0 )
4	3	a1i	|- ( I e. V -> 0 = if ( x = n , 0 , 0 ) )
5	4	mpteq2dv	|- ( I e. V -> ( x e. I |-> 0 ) = ( x e. I |-> if ( x = n , 0 , 0 ) ) )
6		0nn0	|- 0 e. NN0
7	1	snifpsrbag	|- ( ( I e. V /\ 0 e. NN0 ) -> ( x e. I |-> if ( x = n , 0 , 0 ) ) e. D )
8	6 7	mpan2	|- ( I e. V -> ( x e. I |-> if ( x = n , 0 , 0 ) ) e. D )
9	5 8	eqeltrd	|- ( I e. V -> ( x e. I |-> 0 ) e. D )