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 f R A × B = f A , g B f R f g

Proof

Step Hyp Ref Expression
1 ssv A V
2 ssv B V
3 resmpo A V B V f V , g V x dom f dom g f x R g x A × B = f A , g B x dom f dom g f x R g x
4 1 2 3 mp2an f V , g V x dom f dom g f x R g x A × B = f A , g B x dom f dom g f x R g x
5 df-of f R = f V , g V x dom f dom g f x R g x
6 5 reseq1i f R A × B = f V , g V x dom f dom g f x R g x A × B
7 eqid A = A
8 eqid B = B
9 vex f V
10 vex g V
11 9 dmex dom f V
12 11 inex1 dom f dom g V
13 12 mptex x dom f dom g f x R g x V
14 5 ovmpt4g f V g V x dom f dom g f x R g x V f R f g = x dom f dom g f x R g x
15 9 10 13 14 mp3an f R f g = x dom f dom g f x R g x
16 7 8 15 mpoeq123i f A , g B f R f g = f A , g B x dom f dom g f x R g x
17 4 6 16 3eqtr4i f R A × B = f A , g B f R f g