Definition df-of 5654

Description: Define the function operation map. The definition is designed so that if R is a binary operation, then o F 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.)

Assertion

Ref	Expression
df-of	|- o F R = (f e. _V , g e. _V |-> (x e. ( dom f i^i dom g) |-> ((f ` x) R(g ` x))))

Distinct variable group:   f,g,x, R

Detailed syntax breakdown of Definition df-of

Step	Hyp	Ref	Expression
1		cR	. . 3 class R
2	1	cof 5652	. 2 class o F R
3		vf	. . 3 setvar f
4		vg	. . 3 setvar g
5		cvv 2551	. . 3 class _V
6		vx	. . . 4 setvar x
7	3	cv 1241	. . . . . 6 class f
8	7	cdm 4288	. . . . 5 class dom f
9	4	cv 1241	. . . . . 6 class g
10	9	cdm 4288	. . . . 5 class dom g
11	8, 10	cin 2910	. . . 4 class ( dom f i^i dom g)
12	6	cv 1241	. . . . . 6 class x
13	12, 7	cfv 4845	. . . . 5 class (f ` x)
14	12, 9	cfv 4845	. . . . 5 class (g ` x)
15	13, 14, 1	co 5455	. . . 4 class ((f ` x) R(g ` x))
16	6, 11, 15	cmpt 3809	. . 3 class (x e. ( dom f i^i dom g) |-> ((f ` x) R(g ` x)))
17	3, 4, 5, 5, 16	cmpt2 5457	. 2 class (f e. _V , g e. _V |-> (x e. ( dom f i^i dom g) |-> ((f ` x) R(g ` x))))
18	2, 17	wceq 1242	1 wff o F R = (f e. _V , g e. _V |-> (x e. ( dom f i^i dom g) |-> ((f ` x) R(g ` x))))

This definition is referenced by:  ofeq  5656  ofexg  5658  offval  5661  offval3  5703  ofmres  5705