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 𝑅 ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑓 ∈ 𝐴 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘f 𝑅 𝑔 ) )

Proof

Step	Hyp	Ref	Expression
1		ssv	⊢ 𝐴 ⊆ V
2		ssv	⊢ 𝐵 ⊆ V
3		resmpo	⊢ ( ( 𝐴 ⊆ V ∧ 𝐵 ⊆ V ) → ( ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑓 ∈ 𝐴 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) )
4	1 2 3	mp2an	⊢ ( ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑓 ∈ 𝐴 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
5		df-of	⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
6	5	reseq1i	⊢ ( ∘f 𝑅 ↾ ( 𝐴 × 𝐵 ) ) = ( ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) ↾ ( 𝐴 × 𝐵 ) )
7		eqid	⊢ 𝐴 = 𝐴
8		eqid	⊢ 𝐵 = 𝐵
9		vex	⊢ 𝑓 ∈ V
10		vex	⊢ 𝑔 ∈ V
11	9	dmex	⊢ dom 𝑓 ∈ V
12	11	inex1	⊢ ( dom 𝑓 ∩ dom 𝑔 ) ∈ V
13	12	mptex	⊢ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ∈ V
14	5	ovmpt4g	⊢ ( ( 𝑓 ∈ V ∧ 𝑔 ∈ V ∧ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ∈ V ) → ( 𝑓 ∘f 𝑅 𝑔 ) = ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
15	9 10 13 14	mp3an	⊢ ( 𝑓 ∘f 𝑅 𝑔 ) = ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) )
16	7 8 15	mpoeq123i	⊢ ( 𝑓 ∈ 𝐴 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘f 𝑅 𝑔 ) ) = ( 𝑓 ∈ 𝐴 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
17	4 6 16	3eqtr4i	⊢ ( ∘f 𝑅 ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑓 ∈ 𝐴 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘f 𝑅 𝑔 ) )