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