MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ofr Structured version   Unicode version

Definition df-ofr 6546
Description: Define the function relation map. The definition is designed so that if  R is a binary relation, then  oR R 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  |-  oR R  =  { <. f ,  g >.  |  A. x  e.  ( dom  f  i^i  dom  g )
( f `  x
) R ( g `
 x ) }
Distinct variable group:    f, g, x, R

Detailed syntax breakdown of Definition df-ofr
StepHypRef Expression
1 cR . . 3  class  R
21cofr 6544 . 2  class  oR R
3 vx . . . . . . 7  setvar  x
43cv 1436 . . . . . 6  class  x
5 vf . . . . . . 7  setvar  f
65cv 1436 . . . . . 6  class  f
74, 6cfv 5601 . . . . 5  class  ( f `
 x )
8 vg . . . . . . 7  setvar  g
98cv 1436 . . . . . 6  class  g
104, 9cfv 5601 . . . . 5  class  ( g `
 x )
117, 10, 1wbr 4426 . . . 4  wff  ( f `
 x ) R ( g `  x
)
126cdm 4854 . . . . 5  class  dom  f
139cdm 4854 . . . . 5  class  dom  g
1412, 13cin 3441 . . . 4  class  ( dom  f  i^i  dom  g
)
1511, 3, 14wral 2782 . . 3  wff  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x )
1615, 5, 8copab 4483 . 2  class  { <. f ,  g >.  |  A. x  e.  ( dom  f  i^i  dom  g )
( f `  x
) R ( g `
 x ) }
172, 16wceq 1437 1  wff  oR R  =  { <. f ,  g >.  |  A. x  e.  ( dom  f  i^i  dom  g )
( f `  x
) R ( g `
 x ) }
Colors of variables: wff setvar class
This definition is referenced by:  ofreq  6548  ofrfval  6553
  Copyright terms: Public domain W3C validator