Definition df-ofr 7698

Description: Define the function relation map. The definition is designed so that if 𝑅 is a binary relation, then ∘_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.)

Assertion

Ref	Expression
df-ofr	⊢ ∘r 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)}

Distinct variable group:   𝑓,𝑔,𝑥,𝑅

Detailed syntax breakdown of Definition df-ofr

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	cofr 7696	. 2 class ∘r 𝑅
3		vx	. . . . . . 7 setvar 𝑥
4	3	cv 1539	. . . . . 6 class 𝑥
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1539	. . . . . 6 class 𝑓
7	4, 6	cfv 6561	. . . . 5 class (𝑓‘𝑥)
8		vg	. . . . . . 7 setvar 𝑔
9	8	cv 1539	. . . . . 6 class 𝑔
10	4, 9	cfv 6561	. . . . 5 class (𝑔‘𝑥)
11	7, 10, 1	wbr 5143	. . . 4 wff (𝑓‘𝑥)𝑅(𝑔‘𝑥)
12	6	cdm 5685	. . . . 5 class dom 𝑓
13	9	cdm 5685	. . . . 5 class dom 𝑔
14	12, 13	cin 3950	. . . 4 class (dom 𝑓 ∩ dom 𝑔)
15	11, 3, 14	wral 3061	. . 3 wff ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)
16	15, 5, 8	copab 5205	. 2 class {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)}
17	2, 16	wceq 1540	1 wff ∘r 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)}

This definition is referenced by:  ofreq  7701  nfofr  7704  ofrfvalg  7705  psrbaglesupp  21942