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 7128
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 7126 . 2 class 𝑟 𝑅
3 vx . . . . . . 7 setvar 𝑥
43cv 1636 . . . . . 6 class 𝑥
5 vf . . . . . . 7 setvar 𝑓
65cv 1636 . . . . . 6 class 𝑓
74, 6cfv 6101 . . . . 5 class (𝑓𝑥)
8 vg . . . . . . 7 setvar 𝑔
98cv 1636 . . . . . 6 class 𝑔
104, 9cfv 6101 . . . . 5 class (𝑔𝑥)
117, 10, 1wbr 4844 . . . 4 wff (𝑓𝑥)𝑅(𝑔𝑥)
126cdm 5311 . . . . 5 class dom 𝑓
139cdm 5311 . . . . 5 class dom 𝑔
1412, 13cin 3768 . . . 4 class (dom 𝑓 ∩ dom 𝑔)
1511, 3, 14wral 3096 . . 3 wff 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)
1615, 5, 8copab 4906 . 2 class {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
172, 16wceq 1637 1 wff 𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  ofreq  7130  nfofr  7133  ofrfval  7135
  Copyright terms: Public domain W3C validator