Metamath Proof Explorer

Theorem ofmres

Description: Equivalent expressions for a restriction of the function operation map. Unlike oF R which is a proper class, ` ( oF R |`( A X. B ) ) can be a set by ofmresex , allowing it to be used as a function or structure argument. By ofmresval , the restricted operation map values are the same as the original values, allowing theorems for oF R to be reused. (Contributed by NM, 20-Oct-2014)

Ref Expression
Assertion ofmres
`|- ( oF R |` ( A X. B ) ) = ( f e. A , g e. B |-> ( f oF R g ) )`

Proof

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 ) )`