Step |
Hyp |
Ref |
Expression |
1 |
|
mvrfval.v |
|- V = ( I mVar R ) |
2 |
|
mvrfval.d |
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
3 |
|
mvrfval.z |
|- .0. = ( 0g ` R ) |
4 |
|
mvrfval.o |
|- .1. = ( 1r ` R ) |
5 |
|
mvrfval.i |
|- ( ph -> I e. W ) |
6 |
|
mvrfval.r |
|- ( ph -> R e. Y ) |
7 |
|
mvrval.x |
|- ( ph -> X e. I ) |
8 |
|
1nn0 |
|- 1 e. NN0 |
9 |
2
|
snifpsrbag |
|- ( ( I e. W /\ 1 e. NN0 ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. D ) |
10 |
5 8 9
|
sylancl |
|- ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. D ) |
11 |
1 2 3 4 5 6 7 10
|
mvrval2 |
|- ( ph -> ( ( V ` X ) ` ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = if ( ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) |
12 |
|
eqid |
|- ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) |
13 |
12
|
iftruei |
|- if ( ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) = .1. |
14 |
11 13
|
eqtrdi |
|- ( ph -> ( ( V ` X ) ` ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = .1. ) |