Metamath Proof Explorer

Definition df-of

Description: Define the function operation map. The definition is designed so that if R is a binary operation, then oF R is the analogous operation on functions which corresponds to applying R pointwise to the values of the functions. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Assertion df-of ⊢ ∘ f ⁡ R = f ∈ V , g ∈ V ⟼ x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x R g ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 0 cof class ∘ f ⁡ R
2 vf setvar f
3 cvv class V
4 vg setvar g
5 vx setvar x
6 2 cv setvar f
7 6 cdm class dom ⁡ f
8 4 cv setvar g
9 8 cdm class dom ⁡ g
10 7 9 cin class dom ⁡ f ∩ dom ⁡ g
11 5 cv setvar x
12 11 6 cfv class f ⁡ x
13 11 8 cfv class g ⁡ x
14 12 13 0 co class f ⁡ x R g ⁡ x
15 5 10 14 cmpt class x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x R g ⁡ x
16 2 4 3 3 15 cmpo class f ∈ V , g ∈ V ⟼ x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x R g ⁡ x
17 1 16 wceq wff ∘ f ⁡ R = f ∈ V , g ∈ V ⟼ x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x R g ⁡ x