Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ofc Structured version   Visualization version   GIF version

Definition df-ofc 29485
 Description: Define the function/constant operation map. The definition is designed so that if 𝑅 is a binary operation, then ∘𝑓/𝑐𝑅 is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.)
Assertion
Ref Expression
df-ofc 𝑓/𝑐𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓𝑥)𝑅𝑐)))
Distinct variable group:   𝑓,𝑐,𝑥,𝑅

Detailed syntax breakdown of Definition df-ofc
StepHypRef Expression
1 cR . . 3 class 𝑅
21cofc 29484 . 2 class 𝑓/𝑐𝑅
3 vf . . 3 setvar 𝑓
4 vc . . 3 setvar 𝑐
5 cvv 3173 . . 3 class V
6 vx . . . 4 setvar 𝑥
73cv 1474 . . . . 5 class 𝑓
87cdm 5038 . . . 4 class dom 𝑓
96cv 1474 . . . . . 6 class 𝑥
109, 7cfv 5804 . . . . 5 class (𝑓𝑥)
114cv 1474 . . . . 5 class 𝑐
1210, 11, 1co 6549 . . . 4 class ((𝑓𝑥)𝑅𝑐)
136, 8, 12cmpt 4643 . . 3 class (𝑥 ∈ dom 𝑓 ↦ ((𝑓𝑥)𝑅𝑐))
143, 4, 5, 5, 13cmpt2 6551 . 2 class (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓𝑥)𝑅𝑐)))
152, 14wceq 1475 1 wff 𝑓/𝑐𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓𝑥)𝑅𝑐)))
 Colors of variables: wff setvar class This definition is referenced by:  ofceq  29486  ofcfval  29487  ofcfval3  29491
 Copyright terms: Public domain W3C validator