Definition df-vol 20924

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

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-vol

Step	Hyp	Ref	Expression
1		cvol 20922	. 2 class vol
2		covol 20921	. . 3 class vol*
3		vy	. . . . . . . 8 setvar y
4	3	cv 1368	. . . . . . 7 class y
5	4, 2	cfv 5413	. . . . . 6 class ( vol* ` y )
6		vx	. . . . . . . . . 10 setvar x
7	6	cv 1368	. . . . . . . . 9 class x
8	4, 7	cin 3322	. . . . . . . 8 class ( y i^i x )
9	8, 2	cfv 5413	. . . . . . 7 class ( vol* ` ( y i^i x ) )
10	4, 7	cdif 3320	. . . . . . . 8 class ( y \ x )
11	10, 2	cfv 5413	. . . . . . 7 class ( vol* ` ( y \ x ) )
12		caddc 9277	. . . . . . 7 class +
13	9, 11, 12	co 6086	. . . . . 6 class ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) )
14	5, 13	wceq 1369	. . . . 5 wff ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) )
15	2	ccnv 4834	. . . . . 6 class `' vol*
16		cr 9273	. . . . . 6 class RR
17	15, 16	cima 4838	. . . . 5 class ( `' vol* " RR )
18	14, 3, 17	wral 2710	. . . 4 wff A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) )
19	18, 6	cab 2424	. . 3 class { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) }
20	2, 19	cres 4837	. 2 class ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } )
21	1, 20	wceq 1369	1 wff vol = ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } )

This definition is referenced by:  ismbl  20984  volres  20986