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