Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ofr Structured version   GIF version

Definition df-ofr 5655
 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 𝑟 𝑅 = {⟨f, g⟩ ∣ x (dom f ∩ dom g)(fx)𝑅(gx)}
Distinct variable group:   f,g,x,𝑅

Detailed syntax breakdown of Definition df-ofr
StepHypRef Expression
1 cR . . 3 class 𝑅
21cofr 5653 . 2 class 𝑟 𝑅
3 vx . . . . . . 7 setvar x
43cv 1241 . . . . . 6 class x
5 vf . . . . . . 7 setvar f
65cv 1241 . . . . . 6 class f
74, 6cfv 4845 . . . . 5 class (fx)
8 vg . . . . . . 7 setvar g
98cv 1241 . . . . . 6 class g
104, 9cfv 4845 . . . . 5 class (gx)
117, 10, 1wbr 3755 . . . 4 wff (fx)𝑅(gx)
126cdm 4288 . . . . 5 class dom f
139cdm 4288 . . . . 5 class dom g
1412, 13cin 2910 . . . 4 class (dom f ∩ dom g)
1511, 3, 14wral 2300 . . 3 wff x (dom f ∩ dom g)(fx)𝑅(gx)
1615, 5, 8copab 3808 . 2 class {⟨f, g⟩ ∣ x (dom f ∩ dom g)(fx)𝑅(gx)}
172, 16wceq 1242 1 wff 𝑟 𝑅 = {⟨f, g⟩ ∣ x (dom f ∩ dom g)(fx)𝑅(gx)}
 Colors of variables: wff set class This definition is referenced by:  ofreq  5657  ofrfval  5662
 Copyright terms: Public domain W3C validator