Step |
Hyp |
Ref |
Expression |
1 |
|
ssv |
|- A C_ _V |
2 |
|
ssv |
|- B C_ _V |
3 |
|
resmpo |
|- ( ( A C_ _V /\ B C_ _V ) -> ( ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |` ( A X. B ) ) = ( f e. A , g e. B |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) ) |
4 |
1 2 3
|
mp2an |
|- ( ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |` ( A X. B ) ) = ( f e. A , g e. B |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
5 |
|
df-of |
|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
6 |
5
|
reseq1i |
|- ( oF R |` ( A X. B ) ) = ( ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |` ( A X. B ) ) |
7 |
|
eqid |
|- A = A |
8 |
|
eqid |
|- B = B |
9 |
|
vex |
|- f e. _V |
10 |
|
vex |
|- g e. _V |
11 |
9
|
dmex |
|- dom f e. _V |
12 |
11
|
inex1 |
|- ( dom f i^i dom g ) e. _V |
13 |
12
|
mptex |
|- ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) e. _V |
14 |
5
|
ovmpt4g |
|- ( ( f e. _V /\ g e. _V /\ ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) e. _V ) -> ( f oF R g ) = ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
15 |
9 10 13 14
|
mp3an |
|- ( f oF R g ) = ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) |
16 |
7 8 15
|
mpoeq123i |
|- ( f e. A , g e. B |-> ( f oF R g ) ) = ( f e. A , g e. B |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
17 |
4 6 16
|
3eqtr4i |
|- ( oF R |` ( A X. B ) ) = ( f e. A , g e. B |-> ( f oF R g ) ) |