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

Definition df-ofc 26560
Description: Define the function/constant operation map. The definition is designed so that if  R is a binary operation, then ∘𝑓/𝑐 R is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.)
Assertion
Ref Expression
df-ofc  |-𝑓/𝑐 R  =  ( f  e.  _V ,  c  e. 
_V  |->  ( x  e. 
dom  f  |->  ( ( f `  x ) R c ) ) )
Distinct variable group:    f, c, x, R

Detailed syntax breakdown of Definition df-ofc
StepHypRef Expression
1 cR . . 3  class  R
21cofc 26559 . 2  class𝑓/𝑐 R
3 vf . . 3  setvar  f
4 vc . . 3  setvar  c
5 cvv 2993 . . 3  class  _V
6 vx . . . 4  setvar  x
73cv 1368 . . . . 5  class  f
87cdm 4861 . . . 4  class  dom  f
96cv 1368 . . . . . 6  class  x
109, 7cfv 5439 . . . . 5  class  ( f `
 x )
114cv 1368 . . . . 5  class  c
1210, 11, 1co 6112 . . . 4  class  ( ( f `  x ) R c )
136, 8, 12cmpt 4371 . . 3  class  ( x  e.  dom  f  |->  ( ( f `  x
) R c ) )
143, 4, 5, 5, 13cmpt2 6114 . 2  class  ( f  e.  _V ,  c  e.  _V  |->  ( x  e.  dom  f  |->  ( ( f `  x
) R c ) ) )
152, 14wceq 1369 1  wff𝑓/𝑐 R  =  ( f  e.  _V ,  c  e. 
_V  |->  ( x  e. 
dom  f  |->  ( ( f `  x ) R c ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  ofceq  26561  ofcfval  26562  ofcfval3  26566
  Copyright terms: Public domain W3C validator