Definition df-ofr 5976

Description: Define the function relation map. The definition is designed so that if 𝑅 is a binary relation, then ∘_𝑓 𝑅 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	⊢ ∘𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)}

Distinct variable group:   𝑓,𝑔,𝑥,𝑅

Detailed syntax breakdown of Definition df-ofr

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	cofr 5974	. 2 class ∘𝑟 𝑅
3		vx	. . . . . . 7 setvar 𝑥
4	3	cv 1330	. . . . . 6 class 𝑥
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1330	. . . . . 6 class 𝑓
7	4, 6	cfv 5118	. . . . 5 class (𝑓‘𝑥)
8		vg	. . . . . . 7 setvar 𝑔
9	8	cv 1330	. . . . . 6 class 𝑔
10	4, 9	cfv 5118	. . . . 5 class (𝑔‘𝑥)
11	7, 10, 1	wbr 3924	. . . 4 wff (𝑓‘𝑥)𝑅(𝑔‘𝑥)
12	6	cdm 4534	. . . . 5 class dom 𝑓
13	9	cdm 4534	. . . . 5 class dom 𝑔
14	12, 13	cin 3065	. . . 4 class (dom 𝑓 ∩ dom 𝑔)
15	11, 3, 14	wral 2414	. . 3 wff ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)
16	15, 5, 8	copab 3983	. 2 class {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)}
17	2, 16	wceq 1331	1 wff ∘𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)}

This definition is referenced by:  ofreq  5978  nfofr  5981  ofrfval  5983