Definition df-vol 23041

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 𝐴 ∈ dom vol. (Contributed by Mario Carneiro, 17-Mar-2014.)

Assertion

Ref	Expression
df-vol	⊢ vol = (vol* ↾ {𝑥 ∣ ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-vol

Step	Hyp	Ref	Expression
1		cvol 23039	. 2 class vol
2		covol 23038	. . 3 class vol*
3		vy	. . . . . . . 8 setvar 𝑦
4	3	cv 1474	. . . . . . 7 class 𝑦
5	4, 2	cfv 5804	. . . . . 6 class (vol*‘𝑦)
6		vx	. . . . . . . . . 10 setvar 𝑥
7	6	cv 1474	. . . . . . . . 9 class 𝑥
8	4, 7	cin 3539	. . . . . . . 8 class (𝑦 ∩ 𝑥)
9	8, 2	cfv 5804	. . . . . . 7 class (vol*‘(𝑦 ∩ 𝑥))
10	4, 7	cdif 3537	. . . . . . . 8 class (𝑦 ∖ 𝑥)
11	10, 2	cfv 5804	. . . . . . 7 class (vol*‘(𝑦 ∖ 𝑥))
12		caddc 9818	. . . . . . 7 class +
13	9, 11, 12	co 6549	. . . . . 6 class ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))
14	5, 13	wceq 1475	. . . . 5 wff (vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))
15	2	ccnv 5037	. . . . . 6 class ◡vol*
16		cr 9814	. . . . . 6 class ℝ
17	15, 16	cima 5041	. . . . 5 class (◡vol* “ ℝ)
18	14, 3, 17	wral 2896	. . . 4 wff ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))
19	18, 6	cab 2596	. . 3 class {𝑥 ∣ ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))}
20	2, 19	cres 5040	. 2 class (vol* ↾ {𝑥 ∣ ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))})
21	1, 20	wceq 1475	1 wff vol = (vol* ↾ {𝑥 ∣ ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))})

This definition is referenced by:  ismbl  23101  volres  23103