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 ) ) ) } )