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

Detailed syntax breakdown of Definition df-ofc
StepHypRef Expression
1 cR . . 3 class 𝑅
21cofc 31240 . 2 class f/c 𝑅
3 vf . . 3 setvar 𝑓
4 vc . . 3 setvar 𝑐
5 cvv 3500 . . 3 class V
6 vx . . . 4 setvar 𝑥
73cv 1529 . . . . 5 class 𝑓
87cdm 5554 . . . 4 class dom 𝑓
96cv 1529 . . . . . 6 class 𝑥
109, 7cfv 6352 . . . . 5 class (𝑓𝑥)
114cv 1529 . . . . 5 class 𝑐
1210, 11, 1co 7148 . . . 4 class ((𝑓𝑥)𝑅𝑐)
136, 8, 12cmpt 5143 . . 3 class (𝑥 ∈ dom 𝑓 ↦ ((𝑓𝑥)𝑅𝑐))
143, 4, 5, 5, 13cmpo 7150 . 2 class (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓𝑥)𝑅𝑐)))
152, 14wceq 1530 1 wff f/c 𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓𝑥)𝑅𝑐)))
 Colors of variables: wff setvar class This definition is referenced by:  ofceq  31242  ofcfval  31243  ofcfval3  31247
 Copyright terms: Public domain W3C validator