Definition df-of 6216

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.)

Assertion

Ref	Expression
df-of	|- oF 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 6214	. 2 class oF R
3		vf	. . 3 setvar f
4		vg	. . 3 setvar g
5		cvv 2799	. . 3 class _V
6		vx	. . . 4 setvar x
7	3	cv 1394	. . . . . 6 class f
8	7	cdm 4718	. . . . 5 class dom f
9	4	cv 1394	. . . . . 6 class g
10	9	cdm 4718	. . . . 5 class dom g
11	8, 10	cin 3196	. . . 4 class ( dom f i^i dom g )
12	6	cv 1394	. . . . . 6 class x
13	12, 7	cfv 5317	. . . . 5 class ( f ` x )
14	12, 9	cfv 5317	. . . . 5 class ( g ` x )
15	13, 14, 1	co 6000	. . . 4 class ( ( f ` x ) R ( g ` x ) )
16	6, 11, 15	cmpt 4144	. . 3 class ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) )
17	3, 4, 5, 5, 16	cmpo 6002	. 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 1395	1 wff oF 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:  ofeqd  6218  ofeq  6219  ofexg  6221  nfof  6222  offval  6224  offval3  6277  ofmres  6279