This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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