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

Definition df-fae 29064
Description: Define a builder for an 'almost everywhere' relation between functions, from relations between function values. In this definition, the range of  f and  g is enforced in order to ensure the resulting relation is a set. (Contributed by Thierry Arnoux, 22-Oct-2017.)
Assertion
Ref Expression
df-fae  |- ~ a.e.  =  ( r  e.  _V ,  m  e.  U. ran measures  |->  { <. f ,  g >.  |  ( ( f  e.  ( dom  r  ^m  U. dom  m )  /\  g  e.  ( dom  r  ^m  U.
dom  m ) )  /\  { x  e. 
U. dom  m  | 
( f `  x
) r ( g `
 x ) }a.e. m ) } )
Distinct variable group:    m, r, f, g, x

Detailed syntax breakdown of Definition df-fae
StepHypRef Expression
1 cfae 29057 . 2  class ~ a.e.
2 vr . . 3  setvar  r
3 vm . . 3  setvar  m
4 cvv 3081 . . 3  class  _V
5 cmeas 29013 . . . . 5  class measures
65crn 4851 . . . 4  class  ran measures
76cuni 4216 . . 3  class  U. ran measures
8 vf . . . . . . . 8  setvar  f
98cv 1436 . . . . . . 7  class  f
102cv 1436 . . . . . . . . 9  class  r
1110cdm 4850 . . . . . . . 8  class  dom  r
123cv 1436 . . . . . . . . . 10  class  m
1312cdm 4850 . . . . . . . . 9  class  dom  m
1413cuni 4216 . . . . . . . 8  class  U. dom  m
15 cmap 7477 . . . . . . . 8  class  ^m
1611, 14, 15co 6302 . . . . . . 7  class  ( dom  r  ^m  U. dom  m )
179, 16wcel 1868 . . . . . 6  wff  f  e.  ( dom  r  ^m  U.
dom  m )
18 vg . . . . . . . 8  setvar  g
1918cv 1436 . . . . . . 7  class  g
2019, 16wcel 1868 . . . . . 6  wff  g  e.  ( dom  r  ^m  U.
dom  m )
2117, 20wa 370 . . . . 5  wff  ( f  e.  ( dom  r  ^m  U. dom  m )  /\  g  e.  ( dom  r  ^m  U. dom  m ) )
22 vx . . . . . . . . . 10  setvar  x
2322cv 1436 . . . . . . . . 9  class  x
2423, 9cfv 5598 . . . . . . . 8  class  ( f `
 x )
2523, 19cfv 5598 . . . . . . . 8  class  ( g `
 x )
2624, 25, 10wbr 4420 . . . . . . 7  wff  ( f `
 x ) r ( g `  x
)
2726, 22, 14crab 2779 . . . . . 6  class  { x  e.  U. dom  m  |  ( f `  x
) r ( g `
 x ) }
28 cae 29056 . . . . . 6  class a.e.
2927, 12, 28wbr 4420 . . . . 5  wff  { x  e.  U. dom  m  |  ( f `  x
) r ( g `
 x ) }a.e. m
3021, 29wa 370 . . . 4  wff  ( ( f  e.  ( dom  r  ^m  U. dom  m )  /\  g  e.  ( dom  r  ^m  U.
dom  m ) )  /\  { x  e. 
U. dom  m  | 
( f `  x
) r ( g `
 x ) }a.e. m )
3130, 8, 18copab 4478 . . 3  class  { <. f ,  g >.  |  ( ( f  e.  ( dom  r  ^m  U. dom  m )  /\  g  e.  ( dom  r  ^m  U.
dom  m ) )  /\  { x  e. 
U. dom  m  | 
( f `  x
) r ( g `
 x ) }a.e. m ) }
322, 3, 4, 7, 31cmpt2 6304 . 2  class  ( r  e.  _V ,  m  e.  U. ran measures  |->  { <. f ,  g >.  |  ( ( f  e.  ( dom  r  ^m  U. dom  m )  /\  g  e.  ( dom  r  ^m  U.
dom  m ) )  /\  { x  e. 
U. dom  m  | 
( f `  x
) r ( g `
 x ) }a.e. m ) } )
331, 32wceq 1437 1  wff ~ a.e.  =  ( r  e.  _V ,  m  e.  U. ran measures  |->  { <. f ,  g >.  |  ( ( f  e.  ( dom  r  ^m  U. dom  m )  /\  g  e.  ( dom  r  ^m  U.
dom  m ) )  /\  { x  e. 
U. dom  m  | 
( f `  x
) r ( g `
 x ) }a.e. m ) } )
Colors of variables: wff setvar class
This definition is referenced by:  faeval  29065
  Copyright terms: Public domain W3C validator