Metamath Proof Explorer

Theorem vonvolmbl

Description: A subset of Real numbers is Lebesgue measurable if and only if its corresponding 1-dimensional set is measurable w.r.t. the 1-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses vonvolmbl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
vonvolmbl.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
Assertion vonvolmbl ( 𝜑 → ( ( 𝐵 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) ↔ 𝐵 ∈ dom vol ) )

Proof

Step Hyp Ref Expression
1 vonvolmbl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 vonvolmbl.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
3 vex ⊢ 𝑦 ∈ V
4 3 a1i ⊢ ( 𝜑 → 𝑦 ∈ V )
5 reex ⊢ ℝ ∈ V
6 5 a1i ⊢ ( 𝜑 → ℝ ∈ V )
7 6 2 ssexd ⊢ ( 𝜑 → 𝐵 ∈ V )
8 snfi ⊢ { 𝐴 } ∈ Fin
9 8 a1i ⊢ ( 𝜑 → { 𝐴 } ∈ Fin )
10 9 elexd ⊢ ( 𝜑 → { 𝐴 } ∈ V )
11 4 7 10 inmap ⊢ ( 𝜑 → ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) )
12 11 eqcomd ⊢ ( 𝜑 → ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) = ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) )
13 12 fveq2d ⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) )
14 4 7 1 difmapsn ⊢ ( 𝜑 → ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) )
15 14 eqcomd ⊢ ( 𝜑 → ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) = ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) )
16 15 fveq2d ⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) )
17 13 16 oveq12d ⊢ ( 𝜑 → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) ) ) = ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) ) ) = ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) )
19 ovexd ⊢ ( 𝑦 ∈ 𝒫 ℝ → ( 𝑦 ↑m { 𝐴 } ) ∈ V )
20 5 a1i ⊢ ( 𝑦 ∈ 𝒫 ℝ → ℝ ∈ V )
21 elpwi ⊢ ( 𝑦 ∈ 𝒫 ℝ → 𝑦 ⊆ ℝ )
22 mapss ⊢ ( ( ℝ ∈ V ∧ 𝑦 ⊆ ℝ ) → ( 𝑦 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) )
23 20 21 22 syl2anc ⊢ ( 𝑦 ∈ 𝒫 ℝ → ( 𝑦 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) )
24 19 23 elpwd ⊢ ( 𝑦 ∈ 𝒫 ℝ → ( 𝑦 ↑m { 𝐴 } ) ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) )
25 24 adantl ⊢ ( ( ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( 𝑦 ↑m { 𝐴 } ) ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) )
26 simpl ⊢ ( ( ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) )
27 ineq1 ⊢ ( 𝑥 = ( 𝑦 ↑m { 𝐴 } ) → ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) )
28 27 fveq2d ⊢ ( 𝑥 = ( 𝑦 ↑m { 𝐴 } ) → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) )
29 difeq1 ⊢ ( 𝑥 = ( 𝑦 ↑m { 𝐴 } ) → ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) )
30 29 fveq2d ⊢ ( 𝑥 = ( 𝑦 ↑m { 𝐴 } ) → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) )
31 28 30 oveq12d ⊢ ( 𝑥 = ( 𝑦 ↑m { 𝐴 } ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) )
32 fveq2 ⊢ ( 𝑥 = ( 𝑦 ↑m { 𝐴 } ) → ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) )
33 31 32 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ↑m { 𝐴 } ) → ( ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ↔ ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) ) )
34 33 rspcva ⊢ ( ( ( 𝑦 ↑m { 𝐴 } ) ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) )
35 25 26 34 syl2anc ⊢ ( ( ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) )
36 35 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) )
37 eqidd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) )
38 18 36 37 3eqtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) )
39 38 eqcomd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) = ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) ) ) )
40 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ℝ ) → 𝐴 ∈ 𝑉 )
41 21 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ℝ ) → 𝑦 ⊆ ℝ )
42 40 41 ovnovol ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝑦 ) )
43 42 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑦 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝑦 ) )
44 41 ssinss1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ℝ ) → ( 𝑦 ∩ 𝐵 ) ⊆ ℝ )
45 40 44 ovnovol ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) ) = ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) )
46 41 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ℝ ) → ( 𝑦 ∖ 𝐵 ) ⊆ ℝ )
47 40 46 ovnovol ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) ) = ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) )
48 45 47 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) ) ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) )
49 48 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∩ 𝐵 ) ↑m { 𝐴 } ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑦 ∖ 𝐵 ) ↑m { 𝐴 } ) ) ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) )
50 39 43 49 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) )
51 50 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) → ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) )
52 51 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) → ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) )
53 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) ∧ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ) → 𝐴 ∈ 𝑉 )
54 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) ∧ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ) → 𝐵 ⊆ ℝ )
55 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) ∧ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ) → ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) )
56 elpwi ⊢ ( 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) → 𝑥 ⊆ ( ℝ ↑m { 𝐴 } ) )
57 56 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) ∧ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ) → 𝑥 ⊆ ( ℝ ↑m { 𝐴 } ) )
58 rneq ⊢ ( 𝑔 = 𝑓 → ran 𝑔 = ran 𝑓 )
59 58 cbviunv ⊢ ∪ 𝑔 ∈ 𝑥 ran 𝑔 = ∪ 𝑓 ∈ 𝑥 ran 𝑓
60 53 54 55 57 59 vonvolmbllem ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) ∧ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ) → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) )
61 60 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) → ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) )
62 61 ex ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) → ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) )
63 52 62 impbid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) )
64 mapss ⊢ ( ( ℝ ∈ V ∧ 𝐵 ⊆ ℝ ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) )
65 6 2 64 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) )
66 9 isvonmbl ⊢ ( 𝜑 → ( ( 𝐵 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) ↔ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) ∧ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) ) )
67 65 66 mpbirand ⊢ ( 𝜑 → ( ( 𝐵 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) ↔ ∀ 𝑥 ∈ 𝒫 ( ℝ ↑m { 𝐴 } ) ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑥 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑥 ) ) )
68 ismbl4 ⊢ ( 𝐵 ∈ dom vol ↔ ( 𝐵 ⊆ ℝ ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) )
69 68 a1i ⊢ ( 𝜑 → ( 𝐵 ∈ dom vol ↔ ( 𝐵 ⊆ ℝ ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) ) )
70 2 69 mpbirand ⊢ ( 𝜑 → ( 𝐵 ∈ dom vol ↔ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) )
71 63 67 70 3bitr4d ⊢ ( 𝜑 → ( ( 𝐵 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) ↔ 𝐵 ∈ dom vol ) )