This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )