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 ( ∘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 𝑅 𝑔 ) )