ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ofr Unicode version

Definition df-ofr 5713
Description: Define the function relation map. The definition is designed so that if  R is a binary relation, then  oF 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 5711 . 2  class  oR R
3 vx . . . . . . 7  setvar  x
43cv 1242 . . . . . 6  class  x
5 vf . . . . . . 7  setvar  f
65cv 1242 . . . . . 6  class  f
74, 6cfv 4902 . . . . 5  class  ( f `
 x )
8 vg . . . . . . 7  setvar  g
98cv 1242 . . . . . 6  class  g
104, 9cfv 4902 . . . . 5  class  ( g `
 x )
117, 10, 1wbr 3764 . . . 4  wff  ( f `
 x ) R ( g `  x
)
126cdm 4345 . . . . 5  class  dom  f
139cdm 4345 . . . . 5  class  dom  g
1412, 13cin 2916 . . . 4  class  ( dom  f  i^i  dom  g
)
1511, 3, 14wral 2306 . . 3  wff  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x )
1615, 5, 8copab 3817 . 2  class  { <. f ,  g >.  |  A. x  e.  ( dom  f  i^i  dom  g )
( f `  x
) R ( g `
 x ) }
172, 16wceq 1243 1  wff  oR 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  5715  ofrfval  5720
  Copyright terms: Public domain W3C validator