Definition df-ofr

Description: Define the function relation map. The definition is designed so that if R is a binary relation, then oR R is the analogous relation on functions which is true when each element of the left function relates to the corresponding element of the right function. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Assertion	df-ofr	|- oR R = { <. f , g >. | A. 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	cofr	|- oR R
2		vf	|- f
3		vg	|- g
4		vx	|- x
5	2	cv	|- f
6	5	cdm	|- dom f
7	3	cv	|- g
8	7	cdm	|- dom g
9	6 8	cin	|- ( dom f i^i dom g )
10	4	cv	|- x
11	10 5	cfv	|- ( f ` x )
12	10 7	cfv	|- ( g ` x )
13	11 12 0	wbr	|- ( f ` x ) R ( g ` x )
14	13 4 9	wral	|- A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x )
15	14 2 3	copab	|- { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
16	1 15	wceq	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }