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

Definition df-ofr 5983
 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 5981 . 2 class 𝑟 𝑅
3 vx . . . . . . 7 setvar 𝑥
43cv 1330 . . . . . 6 class 𝑥
5 vf . . . . . . 7 setvar 𝑓
65cv 1330 . . . . . 6 class 𝑓
74, 6cfv 5123 . . . . 5 class (𝑓𝑥)
8 vg . . . . . . 7 setvar 𝑔
98cv 1330 . . . . . 6 class 𝑔
104, 9cfv 5123 . . . . 5 class (𝑔𝑥)
117, 10, 1wbr 3929 . . . 4 wff (𝑓𝑥)𝑅(𝑔𝑥)
126cdm 4539 . . . . 5 class dom 𝑓
139cdm 4539 . . . . 5 class dom 𝑔
1412, 13cin 3070 . . . 4 class (dom 𝑓 ∩ dom 𝑔)
1511, 3, 14wral 2416 . . 3 wff 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)
1615, 5, 8copab 3988 . 2 class {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
172, 16wceq 1331 1 wff 𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
 Colors of variables: wff set class This definition is referenced by:  ofreq  5985  nfofr  5988  ofrfval  5990
 Copyright terms: Public domain W3C validator