This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem volfiniun

Description: The volume of a disjoint finite union of measurable sets is the sum of the measures. (Contributed by Mario Carneiro, 25-Jun-2014) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion volfiniun ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝐴 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) )

Proof

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 biimtrid ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( 𝑤 ∈ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 → ( 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 → 𝑧 ∈ 𝑦 ) ) )
112 111 impd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ( 𝑤 ∈ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) → 𝑧 ∈ 𝑦 ) )
113 90 112 biimtrid ⊢ ( ( ( 𝑦 ∈ 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 eqtrid ⊢ ( ( ( 𝑦 ∈ 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 imbitrrid ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) → ( ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) → ( vol ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
175 61 fveq2i ⊢ ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
176 nfcv ⊢ Ⅎ 𝑚 ( vol ‘ 𝐵 )
177 124 176 120 cbvsum ⊢ Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) = Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
178 175 177 eqeq12i ⊢ ( ( vol ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol ‘ 𝐵 ) ↔ ( vol ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = Σ 𝑚 ∈ 𝑦 ( vol ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
179 58 59 60 cbviun ⊢ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵
180 179 fveq2i ⊢ ( vol ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( vol ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
181 124 176 120 cbvsum ⊢ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 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 ‘ 𝐵 ) )