Metamath Proof Explorer


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 )