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* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvol	⊢ vol
1		covol	⊢ vol*
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4	1	ccnv	⊢ ◡ vol*
5		cr	⊢ ℝ
6	4 5	cima	⊢ ( ◡ vol* “ ℝ )
7	3	cv	⊢ 𝑦
8	7 1	cfv	⊢ ( vol* ‘ 𝑦 )
9	2	cv	⊢ 𝑥
10	7 9	cin	⊢ ( 𝑦 ∩ 𝑥 )
11	10 1	cfv	⊢ ( vol* ‘ ( 𝑦 ∩ 𝑥 ) )
12		caddc	⊢ +
13	7 9	cdif	⊢ ( 𝑦 ∖ 𝑥 )
14	13 1	cfv	⊢ ( vol* ‘ ( 𝑦 ∖ 𝑥 ) )
15	11 14 12	co	⊢ ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) )
16	8 15	wceq	⊢ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) )
17	16 3 6	wral	⊢ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) )
18	17 2	cab	⊢ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) }
19	1 18	cres	⊢ ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )
20	0 19	wceq	⊢ vol = ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )