Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ofr Structured version   Visualization version   GIF version

Definition df-ofr 6940
 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
StepHypRef Expression
1 cR . . 3 class 𝑅
21cofr 6938 . 2 class 𝑟 𝑅
3 vx . . . . . . 7 setvar 𝑥
43cv 1522 . . . . . 6 class 𝑥
5 vf . . . . . . 7 setvar 𝑓
65cv 1522 . . . . . 6 class 𝑓
74, 6cfv 5926 . . . . 5 class (𝑓𝑥)
8 vg . . . . . . 7 setvar 𝑔
98cv 1522 . . . . . 6 class 𝑔
104, 9cfv 5926 . . . . 5 class (𝑔𝑥)
117, 10, 1wbr 4685 . . . 4 wff (𝑓𝑥)𝑅(𝑔𝑥)
126cdm 5143 . . . . 5 class dom 𝑓
139cdm 5143 . . . . 5 class dom 𝑔
1412, 13cin 3606 . . . 4 class (dom 𝑓 ∩ dom 𝑔)
1511, 3, 14wral 2941 . . 3 wff 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)
1615, 5, 8copab 4745 . 2 class {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
172, 16wceq 1523 1 wff 𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
 Colors of variables: wff setvar class This definition is referenced by:  ofreq  6942  ofrfval  6947
 Copyright terms: Public domain W3C validator