Metamath Proof Explorer

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 ⊢ φ → X ∈ Fin
Assertion isvonmbl ⊢ φ → E ∈ dom ⁡ voln ⁡ X ↔ E ⊆ ℝ X ∧ ∀ a ∈ 𝒫 ℝ X voln* ⁡ X ⁡ a ∩ E + 𝑒 voln* ⁡ X ⁡ a ∖ E = voln* ⁡ X ⁡ a

Proof

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