Step |
Hyp |
Ref |
Expression |
1 |
|
dvhvscaval.s |
|- .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) |
2 |
|
fveq1 |
|- ( t = U -> ( t ` ( 1st ` g ) ) = ( U ` ( 1st ` g ) ) ) |
3 |
|
coeq1 |
|- ( t = U -> ( t o. ( 2nd ` g ) ) = ( U o. ( 2nd ` g ) ) ) |
4 |
2 3
|
opeq12d |
|- ( t = U -> <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. = <. ( U ` ( 1st ` g ) ) , ( U o. ( 2nd ` g ) ) >. ) |
5 |
|
2fveq3 |
|- ( g = F -> ( U ` ( 1st ` g ) ) = ( U ` ( 1st ` F ) ) ) |
6 |
|
fveq2 |
|- ( g = F -> ( 2nd ` g ) = ( 2nd ` F ) ) |
7 |
6
|
coeq2d |
|- ( g = F -> ( U o. ( 2nd ` g ) ) = ( U o. ( 2nd ` F ) ) ) |
8 |
5 7
|
opeq12d |
|- ( g = F -> <. ( U ` ( 1st ` g ) ) , ( U o. ( 2nd ` g ) ) >. = <. ( U ` ( 1st ` F ) ) , ( U o. ( 2nd ` F ) ) >. ) |
9 |
1
|
dvhvscacbv |
|- .x. = ( t e. E , g e. ( T X. E ) |-> <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. ) |
10 |
|
opex |
|- <. ( U ` ( 1st ` F ) ) , ( U o. ( 2nd ` F ) ) >. e. _V |
11 |
4 8 9 10
|
ovmpo |
|- ( ( U e. E /\ F e. ( T X. E ) ) -> ( U .x. F ) = <. ( U ` ( 1st ` F ) ) , ( U o. ( 2nd ` F ) ) >. ) |