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