Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
2 | 1 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑦 ∈ V) |
3 | | reex 9906 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℝ ∈
V) |
5 | | vonvolmbl.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
6 | 4, 5 | ssexd 4733 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ V) |
7 | | snfi 7923 |
. . . . . . . . . . . . . . 15
⊢ {𝐴} ∈ Fin |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝐴} ∈ Fin) |
9 | 8 | elexd 3187 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝐴} ∈ V) |
10 | 2, 6, 9 | inmap 38396 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴})) = ((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) |
11 | 10 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∩ 𝐵) ↑𝑚 {𝐴}) = ((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝜑 → ((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) = ((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴})))) |
13 | | vonvolmbl.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
14 | 2, 6, 13 | difmapsn 38399 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴})) = ((𝑦 ∖ 𝐵) ↑𝑚 {𝐴})) |
15 | 14 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∖ 𝐵) ↑𝑚 {𝐴}) = ((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴}))) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝜑 → ((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑𝑚 {𝐴})) = ((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴})))) |
17 | 12, 16 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝜑 → (((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑𝑚 {𝐴}))) = (((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴}))))) |
18 | 17 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑𝑚 {𝐴}))) = (((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴}))))) |
19 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑦 ↑𝑚
{𝐴}) ∈
V |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦
↑𝑚 {𝐴}) ∈ V) |
21 | 3 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 ℝ →
ℝ ∈ V) |
22 | | elpwi 4117 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 ℝ →
𝑦 ⊆
ℝ) |
23 | | mapss 7786 |
. . . . . . . . . . . . 13
⊢ ((ℝ
∈ V ∧ 𝑦 ⊆
ℝ) → (𝑦
↑𝑚 {𝐴}) ⊆ (ℝ
↑𝑚 {𝐴})) |
24 | 21, 22, 23 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦
↑𝑚 {𝐴}) ⊆ (ℝ
↑𝑚 {𝐴})) |
25 | 20, 24 | elpwd 38264 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 ℝ →
(𝑦
↑𝑚 {𝐴}) ∈ 𝒫 (ℝ
↑𝑚 {𝐴})) |
26 | 25 | adantl 481 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝒫 (ℝ ↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ↑𝑚
{𝐴}) ∈ 𝒫
(ℝ ↑𝑚 {𝐴})) |
27 | | simpl 472 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝒫 (ℝ ↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ∧ 𝑦 ∈ 𝒫 ℝ) →
∀𝑥 ∈ 𝒫
(ℝ ↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) |
28 | | ineq1 3769 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ↑𝑚 {𝐴}) → (𝑥 ∩ (𝐵 ↑𝑚 {𝐴})) = ((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ↑𝑚 {𝐴}) → ((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) = ((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴})))) |
30 | | difeq1 3683 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ↑𝑚 {𝐴}) → (𝑥 ∖ (𝐵 ↑𝑚 {𝐴})) = ((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴}))) |
31 | 30 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ↑𝑚 {𝐴}) → ((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴}))) = ((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴})))) |
32 | 29, 31 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ↑𝑚 {𝐴}) → (((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = (((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴}))))) |
33 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ↑𝑚 {𝐴}) → ((voln*‘{𝐴})‘𝑥) = ((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴}))) |
34 | 32, 33 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ↑𝑚 {𝐴}) → ((((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ↔ (((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴})))) |
35 | 34 | rspcva 3280 |
. . . . . . . . . 10
⊢ (((𝑦 ↑𝑚
{𝐴}) ∈ 𝒫
(ℝ ↑𝑚 {𝐴}) ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) → (((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴}))) |
36 | 26, 27, 35 | syl2anc 691 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝒫 (ℝ ↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴}))) |
37 | 36 | adantll 746 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘((𝑦 ↑𝑚 {𝐴}) ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴}))) |
38 | | eqidd 2611 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴})) = ((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴}))) |
39 | 18, 37, 38 | 3eqtrd 2648 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑𝑚 {𝐴}))) = ((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴}))) |
40 | 39 | eqcomd 2616 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴})) = (((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑𝑚 {𝐴})))) |
41 | 13 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → 𝐴 ∈ 𝑉) |
42 | 22 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → 𝑦 ⊆
ℝ) |
43 | 41, 42 | ovnovol 39549 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴})) = (vol*‘𝑦)) |
44 | 43 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘(𝑦 ↑𝑚 {𝐴})) = (vol*‘𝑦)) |
45 | 42 | ssinss1d 38239 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ∩ 𝐵) ⊆ ℝ) |
46 | 41, 45 | ovnovol 39549 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) = (vol*‘(𝑦 ∩ 𝐵))) |
47 | 42 | ssdifssd 3710 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) → (𝑦 ∖ 𝐵) ⊆ ℝ) |
48 | 41, 47 | ovnovol 39549 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑𝑚 {𝐴})) = (vol*‘(𝑦 ∖ 𝐵))) |
49 | 46, 48 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑𝑚 {𝐴}))) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) |
50 | 49 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(((voln*‘{𝐴})‘((𝑦 ∩ 𝐵) ↑𝑚 {𝐴})) +𝑒
((voln*‘{𝐴})‘((𝑦 ∖ 𝐵) ↑𝑚 {𝐴}))) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) |
51 | 40, 44, 50 | 3eqtr3d 2652 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) ∧ 𝑦 ∈ 𝒫 ℝ) →
(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵)))) |
52 | 51 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) → ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) |
53 | 52 | ex 449 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥) → ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵))))) |
54 | 13 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})) → 𝐴 ∈ 𝑉) |
55 | 5 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})) → 𝐵 ⊆ ℝ) |
56 | | simplr 788 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})) → ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) |
57 | | elpwi 4117 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴}) → 𝑥 ⊆ (ℝ ↑𝑚
{𝐴})) |
58 | 57 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})) → 𝑥 ⊆ (ℝ ↑𝑚
{𝐴})) |
59 | | rneq 5272 |
. . . . . . 7
⊢ (𝑔 = 𝑓 → ran 𝑔 = ran 𝑓) |
60 | 59 | cbviunv 4495 |
. . . . . 6
⊢ ∪ 𝑔 ∈ 𝑥 ran 𝑔 = ∪ 𝑓 ∈ 𝑥 ran 𝑓 |
61 | 54, 55, 56, 58, 60 | vonvolmbllem 39550 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) ∧ 𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})) → (((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) |
62 | 61 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) → ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)) |
63 | 62 | ex 449 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵))) → ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥))) |
64 | 53, 63 | impbid 201 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥) ↔ ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵))))) |
65 | | mapss 7786 |
. . . 4
⊢ ((ℝ
∈ V ∧ 𝐵 ⊆
ℝ) → (𝐵
↑𝑚 {𝐴}) ⊆ (ℝ
↑𝑚 {𝐴})) |
66 | 4, 5, 65 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐵 ↑𝑚 {𝐴}) ⊆ (ℝ
↑𝑚 {𝐴})) |
67 | 8 | isvonmbl 39528 |
. . 3
⊢ (𝜑 → ((𝐵 ↑𝑚 {𝐴}) ∈ dom (voln‘{𝐴}) ↔ ((𝐵 ↑𝑚 {𝐴}) ⊆ (ℝ
↑𝑚 {𝐴}) ∧ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥)))) |
68 | 66, 67 | mpbirand 529 |
. 2
⊢ (𝜑 → ((𝐵 ↑𝑚 {𝐴}) ∈ dom (voln‘{𝐴}) ↔ ∀𝑥 ∈ 𝒫 (ℝ
↑𝑚 {𝐴})(((voln*‘{𝐴})‘(𝑥 ∩ (𝐵 ↑𝑚 {𝐴}))) +𝑒
((voln*‘{𝐴})‘(𝑥 ∖ (𝐵 ↑𝑚 {𝐴})))) = ((voln*‘{𝐴})‘𝑥))) |
69 | | ismbl4 38886 |
. . . 4
⊢ (𝐵 ∈ dom vol ↔ (𝐵 ⊆ ℝ ∧
∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵))))) |
70 | 69 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐵 ∈ dom vol ↔ (𝐵 ⊆ ℝ ∧ ∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵)))))) |
71 | 5, 70 | mpbirand 529 |
. 2
⊢ (𝜑 → (𝐵 ∈ dom vol ↔ ∀𝑦 ∈ 𝒫
ℝ(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝐵)) +𝑒
(vol*‘(𝑦 ∖
𝐵))))) |
72 | 64, 68, 71 | 3bitr4d 299 |
1
⊢ (𝜑 → ((𝐵 ↑𝑚 {𝐴}) ∈ dom (voln‘{𝐴}) ↔ 𝐵 ∈ dom vol)) |