| Step |
Hyp |
Ref |
Expression |
| 1 |
|
raleq |
⊢ ( 𝑤 = ∅ → ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑘 ∈ ∅ ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) ) |
| 2 |
|
disjeq1 |
⊢ ( 𝑤 = ∅ → ( Disj 𝑘 ∈ 𝑤 𝐵 ↔ Disj 𝑘 ∈ ∅ 𝐵 ) ) |
| 3 |
1 2
|
anbi12d |
⊢ ( 𝑤 = ∅ → ( ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑤 𝐵 ) ↔ ( ∀ 𝑘 ∈ ∅ ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ∅ 𝐵 ) ) ) |
| 4 |
|
iuneq1 |
⊢ ( 𝑤 = ∅ → ∪ 𝑘 ∈ 𝑤 𝐵 = ∪ 𝑘 ∈ ∅ 𝐵 ) |
| 5 |
4
|
fveq2d |
⊢ ( 𝑤 = ∅ → ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = ( vol ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) ) |
| 6 |
|
sumeq1 |
⊢ ( 𝑤 = ∅ → Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) = Σ 𝑘 ∈ ∅ ( vol ‘ 𝐵 ) ) |
| 7 |
5 6
|
eqeq12d |
⊢ ( 𝑤 = ∅ → ( ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) ↔ ( vol ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) = Σ 𝑘 ∈ ∅ ( vol ‘ 𝐵 ) ) ) |
| 8 |
3 7
|
imbi12d |
⊢ ( 𝑤 = ∅ → ( ( ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑤 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) ) ↔ ( ( ∀ 𝑘 ∈ ∅ ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ∅ 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) = Σ 𝑘 ∈ ∅ ( vol ‘ 𝐵 ) ) ) ) |
| 9 |
|
raleq |
⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑘 ∈ 𝑦 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) ) |
| 10 |
|
disjeq1 |
⊢ ( 𝑤 = 𝑦 → ( Disj 𝑘 ∈ 𝑤 𝐵 ↔ Disj 𝑘 ∈ 𝑦 𝐵 ) ) |
| 11 |
9 10
|
anbi12d |
⊢ ( 𝑤 = 𝑦 → ( ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑤 𝐵 ) ↔ ( ∀ 𝑘 ∈ 𝑦 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑦 𝐵 ) ) ) |
| 12 |
|
iuneq1 |
⊢ ( 𝑤 = 𝑦 → ∪ 𝑘 ∈ 𝑤 𝐵 = ∪ 𝑘 ∈ 𝑦 𝐵 ) |
| 13 |
12
|
fveq2d |
⊢ ( 𝑤 = 𝑦 → ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ) |
| 14 |
|
sumeq1 |
⊢ ( 𝑤 = 𝑦 → Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ) |
| 15 |
13 14
|
eqeq12d |
⊢ ( 𝑤 = 𝑦 → ( ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) ↔ ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ) ) |
| 16 |
11 15
|
imbi12d |
⊢ ( 𝑤 = 𝑦 → ( ( ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑤 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) ) ↔ ( ( ∀ 𝑘 ∈ 𝑦 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑦 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ) ) ) |
| 17 |
|
raleq |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) ) |
| 18 |
|
disjeq1 |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( Disj 𝑘 ∈ 𝑤 𝐵 ↔ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) |
| 19 |
17 18
|
anbi12d |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑤 𝐵 ) ↔ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ) |
| 20 |
|
iuneq1 |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ∪ 𝑘 ∈ 𝑤 𝐵 = ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) |
| 21 |
20
|
fveq2d |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) |
| 22 |
|
sumeq1 |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) ) |
| 23 |
21 22
|
eqeq12d |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) ↔ ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) ) ) |
| 24 |
19 23
|
imbi12d |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑤 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) ) ↔ ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) ) ) ) |
| 25 |
|
raleq |
⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) ) |
| 26 |
|
disjeq1 |
⊢ ( 𝑤 = 𝐴 → ( Disj 𝑘 ∈ 𝑤 𝐵 ↔ Disj 𝑘 ∈ 𝐴 𝐵 ) ) |
| 27 |
25 26
|
anbi12d |
⊢ ( 𝑤 = 𝐴 → ( ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑤 𝐵 ) ↔ ( ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝐴 𝐵 ) ) ) |
| 28 |
|
iuneq1 |
⊢ ( 𝑤 = 𝐴 → ∪ 𝑘 ∈ 𝑤 𝐵 = ∪ 𝑘 ∈ 𝐴 𝐵 ) |
| 29 |
28
|
fveq2d |
⊢ ( 𝑤 = 𝐴 → ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) |
| 30 |
|
sumeq1 |
⊢ ( 𝑤 = 𝐴 → Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) ) |
| 31 |
29 30
|
eqeq12d |
⊢ ( 𝑤 = 𝐴 → ( ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) ↔ ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) ) ) |
| 32 |
27 31
|
imbi12d |
⊢ ( 𝑤 = 𝐴 → ( ( ( ∀ 𝑘 ∈ 𝑤 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑤 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑤 𝐵 ) = Σ 𝑘 ∈ 𝑤 ( vol ‘ 𝐵 ) ) ↔ ( ( ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝐴 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) ) ) ) |
| 33 |
|
0mbl |
⊢ ∅ ∈ dom vol |
| 34 |
|
mblvol |
⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) ) |
| 35 |
33 34
|
ax-mp |
⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) |
| 36 |
|
ovol0 |
⊢ ( vol* ‘ ∅ ) = 0 |
| 37 |
35 36
|
eqtri |
⊢ ( vol ‘ ∅ ) = 0 |
| 38 |
|
0iun |
⊢ ∪ 𝑘 ∈ ∅ 𝐵 = ∅ |
| 39 |
38
|
fveq2i |
⊢ ( vol ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) = ( vol ‘ ∅ ) |
| 40 |
|
sum0 |
⊢ Σ 𝑘 ∈ ∅ ( vol ‘ 𝐵 ) = 0 |
| 41 |
37 39 40
|
3eqtr4i |
⊢ ( vol ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) = Σ 𝑘 ∈ ∅ ( vol ‘ 𝐵 ) |
| 42 |
41
|
a1i |
⊢ ( ( ∀ 𝑘 ∈ ∅ ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ∅ 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) = Σ 𝑘 ∈ ∅ ( vol ‘ 𝐵 ) ) |
| 43 |
|
ssun1 |
⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) |
| 44 |
|
ssralv |
⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) → ∀ 𝑘 ∈ 𝑦 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) ) |
| 45 |
43 44
|
ax-mp |
⊢ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) → ∀ 𝑘 ∈ 𝑦 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) |
| 46 |
|
disjss1 |
⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → Disj 𝑘 ∈ 𝑦 𝐵 ) ) |
| 47 |
43 46
|
ax-mp |
⊢ ( Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → Disj 𝑘 ∈ 𝑦 𝐵 ) |
| 48 |
45 47
|
anim12i |
⊢ ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( ∀ 𝑘 ∈ 𝑦 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑦 𝐵 ) ) |
| 49 |
48
|
imim1i |
⊢ ( ( ( ∀ 𝑘 ∈ 𝑦 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑦 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ) → ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ) ) |
| 50 |
|
oveq1 |
⊢ ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) → ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) |
| 51 |
|
iunxun |
⊢ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ∪ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 52 |
|
vex |
⊢ 𝑧 ∈ V |
| 53 |
|
csbeq1 |
⊢ ( 𝑚 = 𝑧 → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) |
| 54 |
52 53
|
iunxsn |
⊢ ∪ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 |
| 55 |
54
|
uneq2i |
⊢ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ∪ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) |
| 56 |
51 55
|
eqtri |
⊢ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) |
| 57 |
56
|
fveq2i |
⊢ ( vol ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol ‘ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) |
| 58 |
|
nfcv |
⊢ Ⅎ 𝑚 𝐵 |
| 59 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 |
| 60 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 61 |
58 59 60
|
cbviun |
⊢ ∪ 𝑘 ∈ 𝑦 𝐵 = ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 |
| 62 |
|
simpll |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → 𝑦 ∈ Fin ) |
| 63 |
|
simprl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) |
| 64 |
|
simpl |
⊢ ( ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) → 𝐵 ∈ dom vol ) |
| 65 |
64
|
ralimi |
⊢ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) |
| 66 |
63 65
|
syl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) |
| 67 |
|
ssralv |
⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) ) |
| 68 |
43 66 67
|
mpsyl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) |
| 69 |
|
finiunmbl |
⊢ ( ( 𝑦 ∈ Fin ∧ ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) → ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) |
| 70 |
62 68 69
|
syl2anc |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) |
| 71 |
61 70
|
eqeltrrid |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ) |
| 72 |
|
ssun2 |
⊢ { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } ) |
| 73 |
|
vsnid |
⊢ 𝑧 ∈ { 𝑧 } |
| 74 |
72 73
|
sselii |
⊢ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) |
| 75 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵 |
| 76 |
75
|
nfel1 |
⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol |
| 77 |
|
nfcv |
⊢ Ⅎ 𝑘 vol |
| 78 |
77 75
|
nffv |
⊢ Ⅎ 𝑘 ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) |
| 79 |
78
|
nfel1 |
⊢ Ⅎ 𝑘 ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ |
| 80 |
76 79
|
nfan |
⊢ Ⅎ 𝑘 ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 81 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) |
| 82 |
81
|
eleq1d |
⊢ ( 𝑘 = 𝑧 → ( 𝐵 ∈ dom vol ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol ) ) |
| 83 |
81
|
fveq2d |
⊢ ( 𝑘 = 𝑧 → ( vol ‘ 𝐵 ) = ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) |
| 84 |
83
|
eleq1d |
⊢ ( 𝑘 = 𝑧 → ( ( vol ‘ 𝐵 ) ∈ ℝ ↔ ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 85 |
82 84
|
anbi12d |
⊢ ( 𝑘 = 𝑧 → ( ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) ) |
| 86 |
80 85
|
rspc |
⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) ) |
| 87 |
74 63 86
|
mpsyl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 88 |
87
|
simpld |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol ) |
| 89 |
|
simplr |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ¬ 𝑧 ∈ 𝑦 ) |
| 90 |
|
elin |
⊢ ( 𝑤 ∈ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑤 ∈ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) |
| 91 |
|
eliun |
⊢ ( 𝑤 ∈ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ↔ ∃ 𝑚 ∈ 𝑦 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 92 |
|
simplrr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) |
| 93 |
|
nfcv |
⊢ Ⅎ 𝑛 𝐵 |
| 94 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐵 |
| 95 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑛 → 𝐵 = ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) |
| 96 |
93 94 95
|
cbvdisj |
⊢ ( Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↔ Disj 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) |
| 97 |
92 96
|
sylib |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → Disj 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) |
| 98 |
|
simpr1 |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 𝑚 ∈ 𝑦 ) |
| 99 |
|
elun1 |
⊢ ( 𝑚 ∈ 𝑦 → 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) |
| 100 |
98 99
|
syl |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) |
| 101 |
74
|
a1i |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ) |
| 102 |
|
simpr2 |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 103 |
|
simpr3 |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) |
| 104 |
|
csbeq1 |
⊢ ( 𝑛 = 𝑚 → ⦋ 𝑛 / 𝑘 ⦌ 𝐵 = ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 105 |
|
csbeq1 |
⊢ ( 𝑛 = 𝑧 → ⦋ 𝑛 / 𝑘 ⦌ 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) |
| 106 |
104 105
|
disji |
⊢ ( ( Disj 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ∧ ( 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ ( 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 𝑚 = 𝑧 ) |
| 107 |
97 100 101 102 103 106
|
syl122anc |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 𝑚 = 𝑧 ) |
| 108 |
107 98
|
eqeltrrd |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ ( 𝑚 ∈ 𝑦 ∧ 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 𝑧 ∈ 𝑦 ) |
| 109 |
108
|
3exp2 |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( 𝑚 ∈ 𝑦 → ( 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 → ( 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 → 𝑧 ∈ 𝑦 ) ) ) ) |
| 110 |
109
|
rexlimdv |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ∃ 𝑚 ∈ 𝑦 𝑤 ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 → ( 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 → 𝑧 ∈ 𝑦 ) ) ) |
| 111 |
91 110
|
syl5bi |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( 𝑤 ∈ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 → ( 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 → 𝑧 ∈ 𝑦 ) ) ) |
| 112 |
111
|
impd |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ( 𝑤 ∈ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) → 𝑧 ∈ 𝑦 ) ) |
| 113 |
90 112
|
syl5bi |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( 𝑤 ∈ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) → 𝑧 ∈ 𝑦 ) ) |
| 114 |
89 113
|
mtod |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ¬ 𝑤 ∈ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) |
| 115 |
114
|
eq0rdv |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) = ∅ ) |
| 116 |
|
mblvol |
⊢ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol → ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) |
| 117 |
71 116
|
syl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) |
| 118 |
|
nfv |
⊢ Ⅎ 𝑚 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) |
| 119 |
59
|
nfel1 |
⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol |
| 120 |
77 59
|
nffv |
⊢ Ⅎ 𝑘 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 121 |
120
|
nfel1 |
⊢ Ⅎ 𝑘 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ |
| 122 |
119 121
|
nfan |
⊢ Ⅎ 𝑘 ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 123 |
60
|
eleq1d |
⊢ ( 𝑘 = 𝑚 → ( 𝐵 ∈ dom vol ↔ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ) ) |
| 124 |
60
|
fveq2d |
⊢ ( 𝑘 = 𝑚 → ( vol ‘ 𝐵 ) = ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) |
| 125 |
124
|
eleq1d |
⊢ ( 𝑘 = 𝑚 → ( ( vol ‘ 𝐵 ) ∈ ℝ ↔ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 126 |
123 125
|
anbi12d |
⊢ ( 𝑘 = 𝑚 → ( ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) ) |
| 127 |
118 122 126
|
cbvralw |
⊢ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 128 |
63 127
|
sylib |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 129 |
128
|
r19.21bi |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 130 |
129
|
simpld |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ) |
| 131 |
|
mblss |
⊢ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) |
| 132 |
130 131
|
syl |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) |
| 133 |
99 132
|
sylan2 |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ 𝑚 ∈ 𝑦 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) |
| 134 |
133
|
ralrimiva |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∀ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) |
| 135 |
|
iunss |
⊢ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ↔ ∀ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) |
| 136 |
134 135
|
sylibr |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) |
| 137 |
|
mblvol |
⊢ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol → ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) |
| 138 |
137
|
eleq1d |
⊢ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol → ( ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ↔ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 139 |
138
|
biimpa |
⊢ ( ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 140 |
129 139
|
syl |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 141 |
99 140
|
sylan2 |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ 𝑚 ∈ 𝑦 ) → ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 142 |
62 141
|
fsumrecl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 143 |
131
|
adantr |
⊢ ( ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) |
| 144 |
143 139
|
jca |
⊢ ( ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 145 |
144
|
ralimi |
⊢ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) → ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 146 |
128 145
|
syl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 147 |
|
ssralv |
⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) → ∀ 𝑚 ∈ 𝑦 ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) ) |
| 148 |
43 146 147
|
mpsyl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ∀ 𝑚 ∈ 𝑦 ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) |
| 149 |
|
ovolfiniun |
⊢ ( ( 𝑦 ∈ Fin ∧ ∀ 𝑚 ∈ 𝑦 ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ≤ Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) |
| 150 |
62 148 149
|
syl2anc |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ≤ Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) |
| 151 |
|
ovollecl |
⊢ ( ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ∧ ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ≤ Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) → ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 152 |
136 142 150 151
|
syl3anc |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 153 |
117 152
|
eqeltrd |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 154 |
87
|
simprd |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 155 |
|
volun |
⊢ ( ( ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol ∧ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) = ∅ ) ∧ ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ∧ ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) |
| 156 |
71 88 115 153 154 155
|
syl32anc |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( vol ‘ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) |
| 157 |
57 156
|
syl5eq |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( vol ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) |
| 158 |
|
disjsn |
⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 ) |
| 159 |
89 158
|
sylibr |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ ) |
| 160 |
|
eqidd |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( 𝑦 ∪ { 𝑧 } ) = ( 𝑦 ∪ { 𝑧 } ) ) |
| 161 |
|
snfi |
⊢ { 𝑧 } ∈ Fin |
| 162 |
|
unfi |
⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) |
| 163 |
62 161 162
|
sylancl |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) |
| 164 |
129
|
simprd |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) |
| 165 |
164
|
recnd |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℂ ) |
| 166 |
159 160 163 165
|
fsumsplit |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + Σ 𝑚 ∈ { 𝑧 } ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) ) |
| 167 |
154
|
recnd |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℂ ) |
| 168 |
53
|
fveq2d |
⊢ ( 𝑚 = 𝑧 → ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) |
| 169 |
168
|
sumsn |
⊢ ( ( 𝑧 ∈ V ∧ ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℂ ) → Σ 𝑚 ∈ { 𝑧 } ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) |
| 170 |
52 167 169
|
sylancr |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → Σ 𝑚 ∈ { 𝑧 } ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) |
| 171 |
170
|
oveq2d |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + Σ 𝑚 ∈ { 𝑧 } ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) = ( Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) |
| 172 |
166 171
|
eqtrd |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) |
| 173 |
157 172
|
eqeq12d |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ( vol ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ↔ ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) ) |
| 174 |
50 173
|
syl5ibr |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) → ( vol ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) ) |
| 175 |
61
|
fveq2i |
⊢ ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 176 |
|
nfcv |
⊢ Ⅎ 𝑚 ( vol ‘ 𝐵 ) |
| 177 |
176 120 124
|
cbvsumi |
⊢ Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) = Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 178 |
175 177
|
eqeq12i |
⊢ ( ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ↔ ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) |
| 179 |
58 59 60
|
cbviun |
⊢ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 |
| 180 |
179
|
fveq2i |
⊢ ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( vol ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 181 |
176 120 124
|
cbvsumi |
⊢ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) = Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) |
| 182 |
180 181
|
eqeq12i |
⊢ ( ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) ↔ ( vol ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) |
| 183 |
174 178 182
|
3imtr4g |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) ) ) |
| 184 |
183
|
ex |
⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) ) ) ) |
| 185 |
184
|
a2d |
⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ) → ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) ) ) ) |
| 186 |
49 185
|
syl5 |
⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ∀ 𝑘 ∈ 𝑦 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝑦 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ) → ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ 𝐵 ) ) ) ) |
| 187 |
8 16 24 32 42 186
|
findcard2s |
⊢ ( 𝐴 ∈ Fin → ( ( ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝐴 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) ) ) |
| 188 |
187
|
3impib |
⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝐴 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) ) |