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 26798
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 26791 . 2  class ~ a.e.
2 vr . . 3  setvar  r
3 vm . . 3  setvar  m
4 cvv 3071 . . 3  class  _V
5 cmeas 26747 . . . . 5  class measures
65crn 4942 . . . 4  class  ran measures
76cuni 4192 . . 3  class  U. ran measures
8 vf . . . . . . . 8  setvar  f
98cv 1369 . . . . . . 7  class  f
102cv 1369 . . . . . . . . 9  class  r
1110cdm 4941 . . . . . . . 8  class  dom  r
123cv 1369 . . . . . . . . . 10  class  m
1312cdm 4941 . . . . . . . . 9  class  dom  m
1413cuni 4192 . . . . . . . 8  class  U. dom  m
15 cmap 7317 . . . . . . . 8  class  ^m
1611, 14, 15co 6193 . . . . . . 7  class  ( dom  r  ^m  U. dom  m )
179, 16wcel 1758 . . . . . 6  wff  f  e.  ( dom  r  ^m  U.
dom  m )
18 vg . . . . . . . 8  setvar  g
1918cv 1369 . . . . . . 7  class  g
2019, 16wcel 1758 . . . . . 6  wff  g  e.  ( dom  r  ^m  U.
dom  m )
2117, 20wa 369 . . . . 5  wff  ( f  e.  ( dom  r  ^m  U. dom  m )  /\  g  e.  ( dom  r  ^m  U. dom  m ) )
22 vx . . . . . . . . . 10  setvar  x
2322cv 1369 . . . . . . . . 9  class  x
2423, 9cfv 5519 . . . . . . . 8  class  ( f `
 x )
2523, 19cfv 5519 . . . . . . . 8  class  ( g `
 x )
2624, 25, 10wbr 4393 . . . . . . 7  wff  ( f `
 x ) r ( g `  x
)
2726, 22, 14crab 2799 . . . . . 6  class  { x  e.  U. dom  m  |  ( f `  x
) r ( g `
 x ) }
28 cae 26790 . . . . . 6  class a.e.
2927, 12, 28wbr 4393 . . . . 5  wff  { x  e.  U. dom  m  |  ( f `  x
) r ( g `
 x ) }a.e. m
3021, 29wa 369 . . . 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 4450 . . 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 6195 . 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 1370 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  26799
  Copyright terms: Public domain W3C validator