Step | Hyp | Ref
| Expression |
1 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
2 | 1 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑦 ∈ V) |
3 | | reex 10820 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℝ ∈
V) |
5 | | vonvolmbl.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
6 | 4, 5 | ssexd 5217 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ V) |
7 | | snfi 8721 |
. . . . . . . . . . . . . . 15
⊢ {𝐴} ∈ Fin |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝐴} ∈ Fin) |
9 | 8 | elexd 3428 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝐴} ∈ V) |
10 | 2, 6, 9 | inmap 42422 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴})) = ((𝑦 ∩ 𝐵) ↑m {𝐴})) |
11 | 10 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∩ 𝐵) ↑m {𝐴}) = ((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) |
12 | 11 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝜑 → ((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) = ((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴})))) |
13 | | vonvolmbl.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
14 | 2, 6, 13 | difmapsn 42425 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})) = ((𝑦 ∖ 𝐵) ↑m {𝐴})) |
15 | 14 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∖ 𝐵) ↑m {𝐴}) = ((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴}))) |
16 | 15 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝜑 → ((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴})) = ((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) |
17 | 12, 16 | oveq12d 7231 |
. . . . . . . . 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 7248 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦 ↑m
{𝐴}) ∈
V) |
20 | 3 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 ℝ →
ℝ ∈ V) |
21 | | elpwi 4522 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 ℝ →
𝑦 ⊆
ℝ) |
22 | | mapss 8570 |
. . . . . . . . . . . . 13
⊢ ((ℝ
∈ V ∧ 𝑦 ⊆
ℝ) → (𝑦
↑m {𝐴})
⊆ (ℝ ↑m {𝐴})) |
23 | 20, 21, 22 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦 ↑m
{𝐴}) ⊆ (ℝ
↑m {𝐴})) |
24 | 19, 23 | elpwd 4521 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦 ↑m
{𝐴}) ∈ 𝒫
(ℝ ↑m {𝐴})) |
25 | 24 | adantl 485 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝒫 (ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ↑m {𝐴}) ∈ 𝒫 (ℝ
↑m {𝐴})) |
26 | | simpl 486 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝒫 (ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ∧ 𝑦 ∈ 𝒫 ℝ) →
∀𝑥 ∈ 𝒫
(ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) |
27 | | ineq1 4120 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → (𝑥 ∩ (𝐵 ↑m {𝐴})) = ((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) |
28 | 27 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → ((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) = ((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴})))) |
29 | | difeq1 4030 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → (𝑥 ∖ (𝐵 ↑m {𝐴})) = ((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴}))) |
30 | 29 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → ((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴}))) = ((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) |
31 | 28, 30 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ↑m {𝐴}) → (((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = (((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴}))))) |
32 | | fveq2 6717 |
. . . . . . . . . . . 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 3535 |
. . . . . . . . . 10
⊢ (((𝑦 ↑m {𝐴}) ∈ 𝒫 (ℝ
↑m {𝐴})
∧ ∀𝑥 ∈
𝒫 (ℝ ↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) → (((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑m {𝐴}) ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑m {𝐴}))) |
35 | 25, 26, 34 | syl2anc 587 |
. . . . . . . . 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 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → 𝐴 ∈ 𝑉) |
41 | 21 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → 𝑦 ⊆
ℝ) |
42 | 40, 41 | ovnovol 43872 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑m {𝐴})) = (vol*‘𝑦)) |
43 | 42 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑m {𝐴})) = (vol*‘𝑦)) |
44 | 41 | ssinss1d 42269 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ∩ 𝐵) ⊆ ℝ) |
45 | 40, 44 | ovnovol 43872 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑m {𝐴})) = (vol*‘(𝑦 ∩ 𝐵))) |
46 | 41 | ssdifssd 4057 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ∖ 𝐵) ⊆ ℝ) |
47 | 40, 46 | ovnovol 43872 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑m {𝐴})) = (vol*‘(𝑦 ∖ 𝐵))) |
48 | 45, 47 | oveq12d 7231 |
. . . . . . 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 3105 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) → ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) |
52 | 51 | ex 416 |
. . 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 4522 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 (ℝ
↑m {𝐴})
→ 𝑥 ⊆ (ℝ
↑m {𝐴})) |
57 | 56 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})) → 𝑥 ⊆ (ℝ
↑m {𝐴})) |
58 | | rneq 5805 |
. . . . . . 7
⊢ (𝑔 = 𝑓 → ran 𝑔 = ran 𝑓) |
59 | 58 | cbviunv 4949 |
. . . . . 6
⊢ ∪ 𝑔 ∈ 𝑥 ran 𝑔 = ∪ 𝑓 ∈ 𝑥 ran 𝑓 |
60 | 53, 54, 55, 57, 59 | vonvolmbllem 43873 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})) →
(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) |
61 | 60 | ralrimiva 3105 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) → ∀𝑥 ∈ 𝒫 (ℝ ↑m
{𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) |
62 | 61 | ex 416 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵))) → ∀𝑥 ∈ 𝒫 (ℝ
↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥))) |
63 | 52, 62 | impbid 215 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝒫 (ℝ
↑m {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑m {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ↔ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵))))) |
64 | | mapss 8570 |
. . . 4
⊢ ((ℝ
∈ V ∧ 𝐵 ⊆
ℝ) → (𝐵
↑m {𝐴})
⊆ (ℝ ↑m {𝐴})) |
65 | 4, 5, 64 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (ℝ ↑m
{𝐴})) |
66 | 8 | isvonmbl 43851 |
. . 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 43209 |
. . . 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 314 |
1
⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ∈ dom (voln‘{𝐴}) ↔ 𝐵 ∈ dom vol)) |