Theorem ismbl

Description: The predicate " A is Lebesgue-measurable". A set is measurable if it splits every other set x in a "nice" way, that is, if the measure of the pieces x i^i A and x \ A sum up to the measure of x (assuming that the measure of x is a real number, so that this addition makes sense). (Contributed by Mario Carneiro, 17-Mar-2014)

	Ref	Expression
Assertion	ismbl	⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ineq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ 𝐴 ) )
2	1	fveq2d	⊢ ( 𝑦 = 𝐴 → ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) = ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) )
3		difeq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∖ 𝑦 ) = ( 𝑥 ∖ 𝐴 ) )
4	3	fveq2d	⊢ ( 𝑦 = 𝐴 → ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) = ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) )
5	2 4	oveq12d	⊢ ( 𝑦 = 𝐴 → ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
6	5	eqeq2d	⊢ ( 𝑦 = 𝐴 → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) ↔ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
7	6	ralbidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
8		df-vol	⊢ vol = ( vol* ↾ { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } )
9	8	dmeqi	⊢ dom vol = dom ( vol* ↾ { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } )
10		dmres	⊢ dom ( vol* ↾ { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ) = ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ dom vol* )
11		ovolf	⊢ vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ )
12	11	fdmi	⊢ dom vol* = 𝒫 ℝ
13	12	ineq2i	⊢ ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ dom vol* ) = ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ 𝒫 ℝ )
14	9 10 13	3eqtri	⊢ dom vol = ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ 𝒫 ℝ )
15		dfrab2	⊢ { 𝑦 ∈ 𝒫 ℝ ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } = ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ 𝒫 ℝ )
16	14 15	eqtr4i	⊢ dom vol = { 𝑦 ∈ 𝒫 ℝ ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) }
17	7 16	elrab2	⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ∈ 𝒫 ℝ ∧ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
18		reex	⊢ ℝ ∈ V
19	18	elpw2	⊢ ( 𝐴 ∈ 𝒫 ℝ ↔ 𝐴 ⊆ ℝ )
20		ffn	⊢ ( vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) → vol* Fn 𝒫 ℝ )
21		elpreima	⊢ ( vol* Fn 𝒫 ℝ → ( 𝑥 ∈ ( ◡ vol* “ ℝ ) ↔ ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) )
22	11 20 21	mp2b	⊢ ( 𝑥 ∈ ( ◡ vol* “ ℝ ) ↔ ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) )
23	22	imbi1i	⊢ ( ( 𝑥 ∈ ( ◡ vol* “ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
24		impexp	⊢ ( ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
25	23 24	bitri	⊢ ( ( 𝑥 ∈ ( ◡ vol* “ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
26	25	ralbii2	⊢ ( ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
27	19 26	anbi12i	⊢ ( ( 𝐴 ∈ 𝒫 ℝ ∧ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
28	17 27	bitri	⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )