Metamath Proof Explorer

Definition df-vol

Description: Define the Lebesgue measure, which is just the outer measure with a peculiar domain of definition. The property of being Lebesgue-measurable can be expressed as A e. dom vol . (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion df-vol 
|- vol = ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvol 
 |-  vol
1 covol 
 |-  vol*
2 vx 
 |-  x
3 vy 
 |-  y
4 1 ccnv 
 |-  `' vol*
5 cr 
 |-  RR
6 4 5 cima 
 |-  ( `' vol* " RR )
7 3 cv 
 |-  y
8 7 1 cfv 
 |-  ( vol* ` y )
9 2 cv 
 |-  x
10 7 9 cin 
 |-  ( y i^i x )
11 10 1 cfv 
 |-  ( vol* ` ( y i^i x ) )
12 caddc 
 |-  +
13 7 9 cdif 
 |-  ( y \ x )
14 13 1 cfv 
 |-  ( vol* ` ( y \ x ) )
15 11 14 12 co 
 |-  ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) )
16 8 15 wceq 
 |-  ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) )
17 16 3 6 wral 
 |-  A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) )
18 17 2 cab 
 |-  { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) }
19 1 18 cres 
 |-  ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } )
20 0 19 wceq 
 |-  vol = ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } )