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 ) |