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

Metamath Proof Explorer

Theorem ovolfiniun

Description: The Lebesgue outer measure function is finitely sub-additive. Finite sum version. (Contributed by Mario Carneiro, 19-Jun-2014)

Ref Expression
Assertion ovolfiniun ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≤ Σ 𝑘 ∈ 𝐴 ( vol* ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 raleq ⊢ ( 𝑥 = ∅ → ( ∀ 𝑘 ∈ 𝑥 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑘 ∈ ∅ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) )
2 iuneq1 ⊢ ( 𝑥 = ∅ → ∪ 𝑘 ∈ 𝑥 𝐵 = ∪ 𝑘 ∈ ∅ 𝐵 )
3 2 fveq2d ⊢ ( 𝑥 = ∅ → ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) = ( vol* ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) )
4 sumeq1 ⊢ ( 𝑥 = ∅ → Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) = Σ 𝑘 ∈ ∅ ( vol* ‘ 𝐵 ) )
5 3 4 breq12d ⊢ ( 𝑥 = ∅ → ( ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) ≤ Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) ↔ ( vol* ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) ≤ Σ 𝑘 ∈ ∅ ( vol* ‘ 𝐵 ) ) )
6 1 5 imbi12d ⊢ ( 𝑥 = ∅ → ( ( ∀ 𝑘 ∈ 𝑥 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) ≤ Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) ) ↔ ( ∀ 𝑘 ∈ ∅ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) ≤ Σ 𝑘 ∈ ∅ ( vol* ‘ 𝐵 ) ) ) )
7 raleq ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ 𝑥 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑘 ∈ 𝑦 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) )
8 iuneq1 ⊢ ( 𝑥 = 𝑦 → ∪ 𝑘 ∈ 𝑥 𝐵 = ∪ 𝑘 ∈ 𝑦 𝐵 )
9 8 fveq2d ⊢ ( 𝑥 = 𝑦 → ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) = ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) )
10 sumeq1 ⊢ ( 𝑥 = 𝑦 → Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) = Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) )
11 9 10 breq12d ⊢ ( 𝑥 = 𝑦 → ( ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) ≤ Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) ↔ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) )
12 7 11 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ∀ 𝑘 ∈ 𝑥 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) ≤ Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) ) ↔ ( ∀ 𝑘 ∈ 𝑦 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) )
13 raleq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ 𝑥 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) )
14 iuneq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∪ 𝑘 ∈ 𝑥 𝐵 = ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
15 14 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) = ( vol* ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) )
16 sumeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ 𝐵 ) )
17 15 16 breq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) ≤ Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) ↔ ( vol* ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ≤ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ 𝐵 ) ) )
18 13 17 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∀ 𝑘 ∈ 𝑥 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) ≤ Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) ) ↔ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ≤ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ 𝐵 ) ) ) )
19 raleq ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑘 ∈ 𝑥 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) )
20 iuneq1 ⊢ ( 𝑥 = 𝐴 → ∪ 𝑘 ∈ 𝑥 𝐵 = ∪ 𝑘 ∈ 𝐴 𝐵 )
21 20 fveq2d ⊢ ( 𝑥 = 𝐴 → ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) = ( vol* ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
22 sumeq1 ⊢ ( 𝑥 = 𝐴 → Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol* ‘ 𝐵 ) )
23 21 22 breq12d ⊢ ( 𝑥 = 𝐴 → ( ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) ≤ Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) ↔ ( vol* ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≤ Σ 𝑘 ∈ 𝐴 ( vol* ‘ 𝐵 ) ) )
24 19 23 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ∀ 𝑘 ∈ 𝑥 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑥 𝐵 ) ≤ Σ 𝑘 ∈ 𝑥 ( vol* ‘ 𝐵 ) ) ↔ ( ∀ 𝑘 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≤ Σ 𝑘 ∈ 𝐴 ( vol* ‘ 𝐵 ) ) ) )
25 0le0 ⊢ 0 ≤ 0
26 0iun ⊢ ∪ 𝑘 ∈ ∅ 𝐵 = ∅
27 26 fveq2i ⊢ ( vol* ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) = ( vol* ‘ ∅ )
28 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
29 27 28 eqtri ⊢ ( vol* ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) = 0
30 sum0 ⊢ Σ 𝑘 ∈ ∅ ( vol* ‘ 𝐵 ) = 0
31 25 29 30 3brtr4i ⊢ ( vol* ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) ≤ Σ 𝑘 ∈ ∅ ( vol* ‘ 𝐵 )
32 31 a1i ⊢ ( ∀ 𝑘 ∈ ∅ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ ∅ 𝐵 ) ≤ Σ 𝑘 ∈ ∅ ( vol* ‘ 𝐵 ) )
33 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
34 ssralv ⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ∀ 𝑘 ∈ 𝑦 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) )
35 33 34 ax-mp ⊢ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ∀ 𝑘 ∈ 𝑦 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
36 35 imim1i ⊢ ( ( ∀ 𝑘 ∈ 𝑦 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) )
37 simprl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
38 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵
39 nfcv ⊢ Ⅎ 𝑘 ℝ
40 38 39 nfss ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ
41 nfcv ⊢ Ⅎ 𝑘 vol*
42 41 38 nffv ⊢ Ⅎ 𝑘 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
43 42 nfel1 ⊢ Ⅎ 𝑘 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ
44 40 43 nfan ⊢ Ⅎ 𝑘 ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
45 csbeq1a ⊢ ( 𝑘 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
46 45 sseq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐵 ⊆ ℝ ↔ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) )
47 45 fveq2d ⊢ ( 𝑘 = 𝑚 → ( vol* ‘ 𝐵 ) = ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
48 47 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ( vol* ‘ 𝐵 ) ∈ ℝ ↔ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) )
49 46 48 anbi12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ↔ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) )
50 44 49 rspc ⊢ ( 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) )
51 37 50 mpan9 ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) )
52 51 simpld ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ )
53 52 ralrimiva ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ )
54 iunss ⊢ ( ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ↔ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ )
55 53 54 sylibr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ )
56 iunss1 ⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
57 33 56 ax-mp ⊢ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵
58 57 55 sstrid ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ )
59 simpll ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → 𝑦 ∈ Fin )
60 elun1 ⊢ ( 𝑚 ∈ 𝑦 → 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) )
61 51 simprd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
62 60 61 sylan2 ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) ∧ 𝑚 ∈ 𝑦 ) → ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
63 59 62 fsumrecl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
64 simprr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) )
65 nfcv ⊢ Ⅎ 𝑚 𝐵
66 65 38 45 cbviun ⊢ ∪ 𝑘 ∈ 𝑦 𝐵 = ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵
67 66 fveq2i ⊢ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) = ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
68 nfcv ⊢ Ⅎ 𝑚 ( vol* ‘ 𝐵 )
69 47 68 42 cbvsum ⊢ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) = Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
70 64 67 69 3brtr3g ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ≤ Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
71 ovollecl ⊢ ( ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ∧ ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ≤ Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) → ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
72 58 63 70 71 syl3anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
73 ssun2 ⊢ { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } )
74 vsnid ⊢ 𝑧 ∈ { 𝑧 }
75 73 74 sselii ⊢ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } )
76 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵
77 76 39 nfss ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ⊆ ℝ
78 41 76 nffv ⊢ Ⅎ 𝑘 ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
79 78 nfel1 ⊢ Ⅎ 𝑘 ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ
80 77 79 nfan ⊢ Ⅎ 𝑘 ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
81 csbeq1a ⊢ ( 𝑘 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
82 81 sseq1d ⊢ ( 𝑘 = 𝑧 → ( 𝐵 ⊆ ℝ ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ⊆ ℝ ) )
83 81 fveq2d ⊢ ( 𝑘 = 𝑧 → ( vol* ‘ 𝐵 ) = ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
84 83 eleq1d ⊢ ( 𝑘 = 𝑧 → ( ( vol* ‘ 𝐵 ) ∈ ℝ ↔ ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) )
85 82 84 anbi12d ⊢ ( 𝑘 = 𝑧 → ( ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ↔ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) )
86 80 85 rspc ⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) )
87 75 37 86 mpsyl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) )
88 87 simprd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
89 72 88 readdcld ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ∈ ℝ )
90 iunxun ⊢ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ∪ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
91 vex ⊢ 𝑧 ∈ V
92 csbeq1 ⊢ ( 𝑚 = 𝑧 → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
93 91 92 iunxsn ⊢ ∪ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵
94 93 uneq2i ⊢ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ∪ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
95 90 94 eqtri ⊢ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
96 95 fveq2i ⊢ ( vol* ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol* ‘ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
97 ovolun ⊢ ( ( ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ∧ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ≤ ( ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
98 58 72 87 97 syl21anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ( ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∪ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ≤ ( ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
99 96 98 eqbrtrid ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ≤ ( ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
100 ovollecl ⊢ ( ( ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ⊆ ℝ ∧ ( ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ≤ ( ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
101 55 89 99 100 syl3anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
102 snfi ⊢ { 𝑧 } ∈ Fin
103 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
104 102 103 mpan2 ⊢ ( 𝑦 ∈ Fin → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
105 104 ad2antrr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
106 105 61 fsumrecl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
107 72 63 88 70 leadd1dd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ≤ ( Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
108 simplr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ¬ 𝑧 ∈ 𝑦 )
109 disjsn ⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
110 108 109 sylibr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
111 eqidd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( 𝑦 ∪ { 𝑧 } ) = ( 𝑦 ∪ { 𝑧 } ) )
112 61 recnd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) ∧ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ∈ ℂ )
113 110 111 105 112 fsumsplit ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + Σ 𝑚 ∈ { 𝑧 } ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
114 88 recnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℂ )
115 92 fveq2d ⊢ ( 𝑚 = 𝑧 → ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
116 115 sumsn ⊢ ( ( 𝑧 ∈ V ∧ ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℂ ) → Σ 𝑚 ∈ { 𝑧 } ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
117 91 114 116 sylancr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → Σ 𝑚 ∈ { 𝑧 } ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
118 117 oveq2d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + Σ 𝑚 ∈ { 𝑧 } ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) = ( Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
119 113 118 eqtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( Σ 𝑚 ∈ 𝑦 ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
120 107 119 breqtrrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( ( vol* ‘ ∪ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) + ( vol* ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ≤ Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
121 101 89 106 99 120 letrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ≤ Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
122 65 38 45 cbviun ⊢ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵
123 122 fveq2i ⊢ ( vol* ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( vol* ‘ ∪ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
124 47 68 42 cbvsum ⊢ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ 𝐵 ) = Σ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
125 121 123 124 3brtr4g ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ∧ ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ≤ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ 𝐵 ) )
126 125 exp32 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) → ( vol* ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ≤ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ 𝐵 ) ) ) )
127 126 a2d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ≤ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ 𝐵 ) ) ) )
128 36 127 syl5 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ∀ 𝑘 ∈ 𝑦 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝑦 𝐵 ) ≤ Σ 𝑘 ∈ 𝑦 ( vol* ‘ 𝐵 ) ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ≤ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( vol* ‘ 𝐵 ) ) ) )
129 6 12 18 24 32 128 findcard2s ⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑘 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≤ Σ 𝑘 ∈ 𝐴 ( vol* ‘ 𝐵 ) ) )
130 129 imp ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≤ Σ 𝑘 ∈ 𝐴 ( vol* ‘ 𝐵 ) )