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	$$⊢{\circ }_{r}R=\left\{⟨f,g⟩|\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Rg\left(x\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1	0	cofr	$$class{\circ }_{r}R$$
2		vf	$$setvarf$$
3		vg	$$setvarg$$
4		vx	$$setvarx$$
5	2	cv	$$setvarf$$
6	5	cdm	$$class\mathrm{dom}f$$
7	3	cv	$$setvarg$$
8	7	cdm	$$class\mathrm{dom}g$$
9	6 8	cin	$$class\left(\mathrm{dom}f\cap \mathrm{dom}g\right)$$
10	4	cv	$$setvarx$$
11	10 5	cfv	$$classf\left(x\right)$$
12	10 7	cfv	$$classg\left(x\right)$$
13	11 12 0	wbr	$$wfff\left(x\right)Rg\left(x\right)$$
14	13 4 9	wral	$$wff\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Rg\left(x\right)$$
15	14 2 3	copab	$$class\left\{⟨f,g⟩|\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Rg\left(x\right)\right\}$$
16	1 15	wceq	$$wff{\circ }_{r}R=\left\{⟨f,g⟩|\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Rg\left(x\right)\right\}$$