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	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1	0	cof	|- oF R
2		vf	|- f
3		cvv	|- _V
4		vg	|- g
5		vx	|- x
6	2	cv	|- f
7	6	cdm	|- dom f
8	4	cv	|- g
9	8	cdm	|- dom g
10	7 9	cin	|- ( dom f i^i dom g )
11	5	cv	|- x
12	11 6	cfv	|- ( f ` x )
13	11 8	cfv	|- ( g ` x )
14	12 13 0	co	|- ( ( f ` x ) R ( g ` x ) )
15	5 10 14	cmpt	|- ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) )
16	2 4 3 3 15	cmpo	|- ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
17	1 16	wceq	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )