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

Definition df-ofr 6769
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 6767 . 2 class 𝑟 𝑅
3 vx . . . . . . 7 setvar 𝑥
43cv 1473 . . . . . 6 class 𝑥
5 vf . . . . . . 7 setvar 𝑓
65cv 1473 . . . . . 6 class 𝑓
74, 6cfv 5786 . . . . 5 class (𝑓𝑥)
8 vg . . . . . . 7 setvar 𝑔
98cv 1473 . . . . . 6 class 𝑔
104, 9cfv 5786 . . . . 5 class (𝑔𝑥)
117, 10, 1wbr 4573 . . . 4 wff (𝑓𝑥)𝑅(𝑔𝑥)
126cdm 5024 . . . . 5 class dom 𝑓
139cdm 5024 . . . . 5 class dom 𝑔
1412, 13cin 3534 . . . 4 class (dom 𝑓 ∩ dom 𝑔)
1511, 3, 14wral 2891 . . 3 wff 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)
1615, 5, 8copab 4632 . 2 class {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
172, 16wceq 1474 1 wff 𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  ofreq  6771  ofrfval  6776
  Copyright terms: Public domain W3C validator