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

Definition df-ofr 7404
 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
StepHypRef Expression
1 cR . . 3 class 𝑅
21cofr 7402 . 2 class r 𝑅
3 vx . . . . . . 7 setvar 𝑥
43cv 1532 . . . . . 6 class 𝑥
5 vf . . . . . . 7 setvar 𝑓
65cv 1532 . . . . . 6 class 𝑓
74, 6cfv 6349 . . . . 5 class (𝑓𝑥)
8 vg . . . . . . 7 setvar 𝑔
98cv 1532 . . . . . 6 class 𝑔
104, 9cfv 6349 . . . . 5 class (𝑔𝑥)
117, 10, 1wbr 5058 . . . 4 wff (𝑓𝑥)𝑅(𝑔𝑥)
126cdm 5549 . . . . 5 class dom 𝑓
139cdm 5549 . . . . 5 class dom 𝑔
1412, 13cin 3934 . . . 4 class (dom 𝑓 ∩ dom 𝑔)
1511, 3, 14wral 3138 . . 3 wff 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)
1615, 5, 8copab 5120 . 2 class {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
172, 16wceq 1533 1 wff r 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
 Colors of variables: wff setvar class This definition is referenced by:  ofreq  7406  nfofr  7409  ofrfval  7411
 Copyright terms: Public domain W3C validator