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