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

Definition df-ofr 6079
Description: Define the function relation map. The definition is designed so that if  R is a binary relation, then  o F 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  |-  o R 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 6077 . 2  class  o R R
3 vx . . . . . . 7  set  x
43cv 1622 . . . . . 6  class  x
5 vf . . . . . . 7  set  f
65cv 1622 . . . . . 6  class  f
74, 6cfv 5255 . . . . 5  class  ( f `
 x )
8 vg . . . . . . 7  set  g
98cv 1622 . . . . . 6  class  g
104, 9cfv 5255 . . . . 5  class  ( g `
 x )
117, 10, 1wbr 4023 . . . 4  wff  ( f `
 x ) R ( g `  x
)
126cdm 4689 . . . . 5  class  dom  f
139cdm 4689 . . . . 5  class  dom  g
1412, 13cin 3151 . . . 4  class  ( dom  f  i^i  dom  g
)
1511, 3, 14wral 2543 . . 3  wff  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x )
1615, 5, 8copab 4076 . 2  class  { <. f ,  g >.  |  A. x  e.  ( dom  f  i^i  dom  g )
( f `  x
) R ( g `
 x ) }
172, 16wceq 1623 1  wff  o R R  =  { <. f ,  g >.  |  A. x  e.  ( dom  f  i^i  dom  g )
( f `  x
) R ( g `
 x ) }
Colors of variables: wff set class
This definition is referenced by:  ofreq  6081  nfofr  6084  ofrfval  6086
  Copyright terms: Public domain W3C validator