| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vex 3484 | . . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V | 
| 2 | 1 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑦 ∈ V) | 
| 3 |  | reex 11246 | . . . . . . . . . . . . . . 15
⊢ ℝ
∈ V | 
| 4 | 3 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ℝ ∈
V) | 
| 5 |  | vonvolmbl.b | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ⊆ ℝ) | 
| 6 | 4, 5 | ssexd 5324 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ V) | 
| 7 |  | snfi 9083 | . . . . . . . . . . . . . . 15
⊢ {𝐴} ∈ Fin | 
| 8 | 7 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → {𝐴} ∈ Fin) | 
| 9 | 8 | elexd 3504 | . . . . . . . . . . . . 13
⊢ (𝜑 → {𝐴} ∈ V) | 
| 10 | 2, 6, 9 | inmap 45214 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴})) = ((𝑦 ∩ 𝐵) ↑m {𝐴})) | 
| 11 | 10 | eqcomd 2743 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∩ 𝐵) ↑m {𝐴}) = ((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) | 
| 12 | 11 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝜑 → ((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) = ((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴})))) | 
| 13 |  | vonvolmbl.a | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 14 | 2, 6, 13 | difmapsn 45217 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})) = ((𝑦 ∖ 𝐵) ↑m {𝐴})) | 
| 15 | 14 | eqcomd 2743 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∖ 𝐵) ↑m {𝐴}) = ((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴}))) | 
| 16 | 15 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝜑 → ((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴})) = ((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) | 
| 17 | 12, 16 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝜑 → (((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴}))) = (((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴}))))) | 
| 18 | 17 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴}))) = (((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴}))))) | 
| 19 |  | ovexd 7466 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦 ↑m
{𝐴}) ∈
V) | 
| 20 | 3 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 ℝ →
ℝ ∈ V) | 
| 21 |  | elpwi 4607 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 ℝ →
𝑦 ⊆
ℝ) | 
| 22 |  | mapss 8929 | . . . . . . . . . . . . 13
⊢ ((ℝ
∈ V ∧ 𝑦 ⊆
ℝ) → (𝑦
↑m {𝐴})
⊆ (ℝ ↑m {𝐴})) | 
| 23 | 20, 21, 22 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦 ↑m
{𝐴}) ⊆ (ℝ
↑m {𝐴})) | 
| 24 | 19, 23 | elpwd 4606 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦 ↑m
{𝐴}) ∈ 𝒫
(ℝ ↑m {𝐴})) | 
| 25 | 24 | adantl 481 | . . . . . . . . . 10
⊢
((∀𝑥 ∈
𝒫 (ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ↑m {𝐴}) ∈ 𝒫 (ℝ
↑m {𝐴})) | 
| 26 |  | simpl 482 | . . . . . . . . . 10
⊢
((∀𝑥 ∈
𝒫 (ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ∧ 𝑦 ∈ 𝒫 ℝ) →
∀𝑥 ∈ 𝒫
(ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) | 
| 27 |  | ineq1 4213 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → (𝑥 ∩ (𝐵 ↑m {𝐴})) = ((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) | 
| 28 | 27 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → ((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) = ((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴})))) | 
| 29 |  | difeq1 4119 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → (𝑥 ∖ (𝐵 ↑m {𝐴})) = ((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴}))) | 
| 30 | 29 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → ((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴}))) = ((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) | 
| 31 | 28, 30 | oveq12d 7449 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → (((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = (((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴}))))) | 
| 32 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → ((voln*‘{𝐴})‘𝑥) = ((voln*‘{𝐴})‘(𝑦 ↑m {𝐴}))) | 
| 33 | 31, 32 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → ((((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ↔ (((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑m {𝐴})))) | 
| 34 | 33 | rspcva 3620 | . . . . . . . . . 10
⊢ (((𝑦 ↑m {𝐴}) ∈ 𝒫 (ℝ
↑m {𝐴})
∧ ∀𝑥 ∈
𝒫 (ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) → (((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑m {𝐴}))) | 
| 35 | 25, 26, 34 | syl2anc 584 | . . . . . . . . 9
⊢
((∀𝑥 ∈
𝒫 (ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑m {𝐴}))) | 
| 36 | 35 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑m {𝐴}))) | 
| 37 |  | eqidd 2738 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑m {𝐴})) = ((voln*‘{𝐴})‘(𝑦 ↑m {𝐴}))) | 
| 38 | 18, 36, 37 | 3eqtrd 2781 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴}))) = ((voln*‘{𝐴})‘(𝑦 ↑m {𝐴}))) | 
| 39 | 38 | eqcomd 2743 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑m {𝐴})) = (((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴})))) | 
| 40 | 13 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → 𝐴 ∈ 𝑉) | 
| 41 | 21 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → 𝑦 ⊆
ℝ) | 
| 42 | 40, 41 | ovnovol 46674 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑m {𝐴})) = (vol*‘𝑦)) | 
| 43 | 42 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑m {𝐴})) = (vol*‘𝑦)) | 
| 44 | 41 | ssinss1d 4247 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ∩ 𝐵) ⊆ ℝ) | 
| 45 | 40, 44 | ovnovol 46674 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) = (vol*‘(𝑦 ∩ 𝐵))) | 
| 46 | 41 | ssdifssd 4147 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ∖ 𝐵) ⊆ ℝ) | 
| 47 | 40, 46 | ovnovol 46674 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴})) = (vol*‘(𝑦 ∖ 𝐵))) | 
| 48 | 45, 47 | oveq12d 7449 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴}))) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) | 
| 49 | 48 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴}))) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) | 
| 50 | 39, 43, 49 | 3eqtr3d 2785 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵)))) | 
| 51 | 50 | ralrimiva 3146 | . . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) → ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) | 
| 52 | 51 | ex 412 | . . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝒫 (ℝ
↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) → ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵))))) | 
| 53 | 13 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})) → 𝐴 ∈ 𝑉) | 
| 54 | 5 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})) → 𝐵 ⊆
ℝ) | 
| 55 |  | simplr 769 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})) → ∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵)))) | 
| 56 |  | elpwi 4607 | . . . . . . 7
⊢ (𝑥 ∈ 𝒫 (ℝ
↑m {𝐴})
→ 𝑥 ⊆ (ℝ
↑m {𝐴})) | 
| 57 | 56 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})) → 𝑥 ⊆ (ℝ
↑m {𝐴})) | 
| 58 |  | rneq 5947 | . . . . . . 7
⊢ (𝑔 = 𝑓 → ran 𝑔 = ran 𝑓) | 
| 59 | 58 | cbviunv 5040 | . . . . . 6
⊢ ∪ 𝑔 ∈ 𝑥 ran 𝑔 = ∪ 𝑓 ∈ 𝑥 ran 𝑓 | 
| 60 | 53, 54, 55, 57, 59 | vonvolmbllem 46675 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})) →
(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) | 
| 61 | 60 | ralrimiva 3146 | . . . 4
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) → ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) | 
| 62 | 61 | ex 412 | . . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵))) → ∀𝑥 ∈ 𝒫 (ℝ
↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥))) | 
| 63 | 52, 62 | impbid 212 | . 2
⊢ (𝜑 → (∀𝑥 ∈ 𝒫 (ℝ
↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ↔ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵))))) | 
| 64 |  | mapss 8929 | . . . 4
⊢ ((ℝ
∈ V ∧ 𝐵 ⊆
ℝ) → (𝐵
↑m {𝐴})
⊆ (ℝ ↑m {𝐴})) | 
| 65 | 4, 5, 64 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (ℝ ↑m
{𝐴})) | 
| 66 | 8 | isvonmbl 46653 | . . 3
⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ∈ dom (voln‘{𝐴}) ↔ ((𝐵 ↑m {𝐴}) ⊆ (ℝ ↑m
{𝐴}) ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)))) | 
| 67 | 65, 66 | mpbirand 707 | . 2
⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ∈ dom (voln‘{𝐴}) ↔ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥))) | 
| 68 |  | ismbl4 46008 | . . . 4
⊢ (𝐵 ∈ dom vol ↔ (𝐵 ⊆ ℝ ∧
∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵))))) | 
| 69 | 68 | a1i 11 | . . 3
⊢ (𝜑 → (𝐵 ∈ dom vol ↔ (𝐵 ⊆ ℝ ∧ ∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵)))))) | 
| 70 | 5, 69 | mpbirand 707 | . 2
⊢ (𝜑 → (𝐵 ∈ dom vol ↔ ∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵))))) | 
| 71 | 63, 67, 70 | 3bitr4d 311 | 1
⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ∈ dom (voln‘{𝐴}) ↔ 𝐵 ∈ dom vol)) |