Theorem isvonmbl

Description: The predicate " A is measurable w.r.t. the n-dimensional Lebesgue measure". 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 . Definition 114E of Fremlin1 p. 25. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypothesis	isvonmbl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion	isvonmbl	⊢ ( 𝜑 → ( 𝐸 ∈ dom ( voln ‘ 𝑋 ) ↔ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isvonmbl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2	1	dmvon	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
3	2	eleq2d	⊢ ( 𝜑 → ( 𝐸 ∈ dom ( voln ‘ 𝑋 ) ↔ 𝐸 ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )
4	1	ovnome	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )
5		eqid	⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) )
6	4 5	caragenel	⊢ ( 𝜑 → ( 𝐸 ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ↔ ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ) )
7		elpwi	⊢ ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) → 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
9	1	unidmovn	⊢ ( 𝜑 → ∪ dom ( voln* ‘ 𝑋 ) = ( ℝ ↑m 𝑋 ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → ∪ dom ( voln* ‘ 𝑋 ) = ( ℝ ↑m 𝑋 ) )
11	8 10	sseqtrd	⊢ ( ( 𝜑 ∧ 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → 𝐸 ⊆ ( ℝ ↑m 𝑋 ) )
12	11	ex	⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) → 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → 𝐸 ⊆ ( ℝ ↑m 𝑋 ) )
14	9	eqcomd	⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) = ∪ dom ( voln* ‘ 𝑋 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → ( ℝ ↑m 𝑋 ) = ∪ dom ( voln* ‘ 𝑋 ) )
16	13 15	sseqtrd	⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
17		ovex	⊢ ( ℝ ↑m 𝑋 ) ∈ V
18	17	ssex	⊢ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) → 𝐸 ∈ V )
19		elpwg	⊢ ( 𝐸 ∈ V → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) ) )
20	18 19	syl	⊢ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) ) )
22	16 21	mpbird	⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) )
23	22	ex	⊢ ( 𝜑 → ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) → 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) )
24	12 23	impbid	⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) )
25	9	pweqd	⊢ ( 𝜑 → 𝒫 ∪ dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )
26		raleq	⊢ ( 𝒫 ∪ dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) → ( ∀ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) )
27	25 26	syl	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) )
28	24 27	anbi12d	⊢ ( 𝜑 → ( ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ↔ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ) )
29	3 6 28	3bitrd	⊢ ( 𝜑 → ( 𝐸 ∈ dom ( voln ‘ 𝑋 ) ↔ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ) )