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 |
5
|
elexd |
|- ( ph -> I e. _V ) |
8 |
6
|
elexd |
|- ( ph -> R e. _V ) |
9 |
5
|
mptexd |
|- ( ph -> ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) e. _V ) |
10 |
|
simpl |
|- ( ( i = I /\ r = R ) -> i = I ) |
11 |
10
|
oveq2d |
|- ( ( i = I /\ r = R ) -> ( NN0 ^m i ) = ( NN0 ^m I ) ) |
12 |
11
|
rabeqdv |
|- ( ( i = I /\ r = R ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) |
13 |
12 2
|
eqtr4di |
|- ( ( i = I /\ r = R ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D ) |
14 |
|
mpteq1 |
|- ( i = I -> ( y e. i |-> if ( y = x , 1 , 0 ) ) = ( y e. I |-> if ( y = x , 1 , 0 ) ) ) |
15 |
14
|
adantr |
|- ( ( i = I /\ r = R ) -> ( y e. i |-> if ( y = x , 1 , 0 ) ) = ( y e. I |-> if ( y = x , 1 , 0 ) ) ) |
16 |
15
|
eqeq2d |
|- ( ( i = I /\ r = R ) -> ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) <-> f = ( y e. I |-> if ( y = x , 1 , 0 ) ) ) ) |
17 |
|
simpr |
|- ( ( i = I /\ r = R ) -> r = R ) |
18 |
17
|
fveq2d |
|- ( ( i = I /\ r = R ) -> ( 1r ` r ) = ( 1r ` R ) ) |
19 |
18 4
|
eqtr4di |
|- ( ( i = I /\ r = R ) -> ( 1r ` r ) = .1. ) |
20 |
17
|
fveq2d |
|- ( ( i = I /\ r = R ) -> ( 0g ` r ) = ( 0g ` R ) ) |
21 |
20 3
|
eqtr4di |
|- ( ( i = I /\ r = R ) -> ( 0g ` r ) = .0. ) |
22 |
16 19 21
|
ifbieq12d |
|- ( ( i = I /\ r = R ) -> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) = if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) |
23 |
13 22
|
mpteq12dv |
|- ( ( i = I /\ r = R ) -> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) = ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) |
24 |
10 23
|
mpteq12dv |
|- ( ( i = I /\ r = R ) -> ( x e. i |-> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) ) = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) ) |
25 |
|
df-mvr |
|- mVar = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) ) ) |
26 |
24 25
|
ovmpoga |
|- ( ( I e. _V /\ R e. _V /\ ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) e. _V ) -> ( I mVar R ) = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) ) |
27 |
7 8 9 26
|
syl3anc |
|- ( ph -> ( I mVar R ) = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) ) |
28 |
1 27
|
syl5eq |
|- ( ph -> V = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) ) |