Step |
Hyp |
Ref |
Expression |
1 |
|
oprab2co.1 |
|- ( ( x e. A /\ y e. B ) -> C e. R ) |
2 |
|
oprab2co.2 |
|- ( ( x e. A /\ y e. B ) -> D e. S ) |
3 |
|
oprab2co.3 |
|- F = ( x e. A , y e. B |-> <. C , D >. ) |
4 |
|
oprab2co.4 |
|- G = ( x e. A , y e. B |-> ( C M D ) ) |
5 |
1 2
|
opelxpd |
|- ( ( x e. A /\ y e. B ) -> <. C , D >. e. ( R X. S ) ) |
6 |
|
df-ov |
|- ( C M D ) = ( M ` <. C , D >. ) |
7 |
6
|
a1i |
|- ( ( x e. A /\ y e. B ) -> ( C M D ) = ( M ` <. C , D >. ) ) |
8 |
7
|
mpoeq3ia |
|- ( x e. A , y e. B |-> ( C M D ) ) = ( x e. A , y e. B |-> ( M ` <. C , D >. ) ) |
9 |
4 8
|
eqtri |
|- G = ( x e. A , y e. B |-> ( M ` <. C , D >. ) ) |
10 |
5 3 9
|
oprabco |
|- ( M Fn ( R X. S ) -> G = ( M o. F ) ) |