Metamath Proof Explorer


Theorem voliunlem1

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypotheses voliunlem.3 ( 𝜑𝐹 : ℕ ⟶ dom vol )
voliunlem.5 ( 𝜑Disj 𝑖 ∈ ℕ ( 𝐹𝑖 ) )
voliunlem1.6 𝐻 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐸 ∩ ( 𝐹𝑛 ) ) ) )
voliunlem1.7 ( 𝜑𝐸 ⊆ ℝ )
voliunlem1.8 ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
Assertion voliunlem1 ( ( 𝜑𝑘 ∈ ℕ ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 voliunlem.3 ( 𝜑𝐹 : ℕ ⟶ dom vol )
2 voliunlem.5 ( 𝜑Disj 𝑖 ∈ ℕ ( 𝐹𝑖 ) )
3 voliunlem1.6 𝐻 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( 𝐸 ∩ ( 𝐹𝑛 ) ) ) )
4 voliunlem1.7 ( 𝜑𝐸 ⊆ ℝ )
5 voliunlem1.8 ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6 difss ( 𝐸 ran 𝐹 ) ⊆ 𝐸
7 5 adantr ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ 𝐸 ) ∈ ℝ )
8 ovolsscl ( ( ( 𝐸 ran 𝐹 ) ⊆ 𝐸𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ∈ ℝ )
9 6 4 7 8 mp3an2ani ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ∈ ℝ )
10 difss ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ⊆ 𝐸
11 ovolsscl ( ( ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ⊆ 𝐸𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ∈ ℝ )
12 10 4 7 11 mp3an2ani ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ∈ ℝ )
13 inss1 ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ⊆ 𝐸
14 ovolsscl ( ( ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ⊆ 𝐸𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ∈ ℝ )
15 13 4 7 14 mp3an2ani ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ∈ ℝ )
16 elfznn ( 𝑛 ∈ ( 1 ... 𝑘 ) → 𝑛 ∈ ℕ )
17 1 ffnd ( 𝜑𝐹 Fn ℕ )
18 fnfvelrn ( ( 𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ ran 𝐹 )
19 17 18 sylan ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ ran 𝐹 )
20 elssuni ( ( 𝐹𝑛 ) ∈ ran 𝐹 → ( 𝐹𝑛 ) ⊆ ran 𝐹 )
21 19 20 syl ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ⊆ ran 𝐹 )
22 16 21 sylan2 ( ( 𝜑𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝐹𝑛 ) ⊆ ran 𝐹 )
23 22 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ⊆ ran 𝐹 )
24 23 adantr ( ( 𝜑𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ⊆ ran 𝐹 )
25 iunss ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ⊆ ran 𝐹 ↔ ∀ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ⊆ ran 𝐹 )
26 24 25 sylibr ( ( 𝜑𝑘 ∈ ℕ ) → 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ⊆ ran 𝐹 )
27 26 sscond ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐸 ran 𝐹 ) ⊆ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) )
28 4 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐸 ⊆ ℝ )
29 10 28 sstrid ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ⊆ ℝ )
30 ovolss ( ( ( 𝐸 ran 𝐹 ) ⊆ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ∧ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ⊆ ℝ ) → ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ≤ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) )
31 27 29 30 syl2anc ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ≤ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) )
32 9 12 15 31 leadd2dd ( ( 𝜑𝑘 ∈ ℕ ) → ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ) ≤ ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ) )
33 oveq2 ( 𝑧 = 1 → ( 1 ... 𝑧 ) = ( 1 ... 1 ) )
34 33 iuneq1d ( 𝑧 = 1 → 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) = 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) )
35 34 eleq1d ( 𝑧 = 1 → ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ↔ 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ∈ dom vol ) )
36 34 ineq2d ( 𝑧 = 1 → ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) = ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) )
37 36 fveq2d ( 𝑧 = 1 → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) ) )
38 fveq2 ( 𝑧 = 1 → ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) )
39 37 38 eqeq12d ( 𝑧 = 1 → ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ↔ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) ) )
40 35 39 anbi12d ( 𝑧 = 1 → ( ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ) ↔ ( 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) ) ) )
41 40 imbi2d ( 𝑧 = 1 → ( ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) ) ) ) )
42 oveq2 ( 𝑧 = 𝑘 → ( 1 ... 𝑧 ) = ( 1 ... 𝑘 ) )
43 42 iuneq1d ( 𝑧 = 𝑘 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) = 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) )
44 43 eleq1d ( 𝑧 = 𝑘 → ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ↔ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ) )
45 43 ineq2d ( 𝑧 = 𝑘 → ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) = ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) )
46 45 fveq2d ( 𝑧 = 𝑘 → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) )
47 fveq2 ( 𝑧 = 𝑘 → ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) )
48 46 47 eqeq12d ( 𝑧 = 𝑘 → ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ↔ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ) )
49 44 48 anbi12d ( 𝑧 = 𝑘 → ( ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ) ) )
50 49 imbi2d ( 𝑧 = 𝑘 → ( ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ) ) ) )
51 oveq2 ( 𝑧 = ( 𝑘 + 1 ) → ( 1 ... 𝑧 ) = ( 1 ... ( 𝑘 + 1 ) ) )
52 51 iuneq1d ( 𝑧 = ( 𝑘 + 1 ) → 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) = 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) )
53 52 eleq1d ( 𝑧 = ( 𝑘 + 1 ) → ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ↔ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∈ dom vol ) )
54 52 ineq2d ( 𝑧 = ( 𝑘 + 1 ) → ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) = ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) )
55 54 fveq2d ( 𝑧 = ( 𝑘 + 1 ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) )
56 fveq2 ( 𝑧 = ( 𝑘 + 1 ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) )
57 55 56 eqeq12d ( 𝑧 = ( 𝑘 + 1 ) → ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ↔ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) ) )
58 53 57 anbi12d ( 𝑧 = ( 𝑘 + 1 ) → ( ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ) ↔ ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) ) ) )
59 58 imbi2d ( 𝑧 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑧 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) ) ) ) )
60 1z 1 ∈ ℤ
61 fzsn ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
62 iuneq1 ( ( 1 ... 1 ) = { 1 } → 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) = 𝑛 ∈ { 1 } ( 𝐹𝑛 ) )
63 60 61 62 mp2b 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) = 𝑛 ∈ { 1 } ( 𝐹𝑛 )
64 1ex 1 ∈ V
65 fveq2 ( 𝑛 = 1 → ( 𝐹𝑛 ) = ( 𝐹 ‘ 1 ) )
66 64 65 iunxsn 𝑛 ∈ { 1 } ( 𝐹𝑛 ) = ( 𝐹 ‘ 1 )
67 63 66 eqtri 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) = ( 𝐹 ‘ 1 )
68 1nn 1 ∈ ℕ
69 ffvelrn ( ( 𝐹 : ℕ ⟶ dom vol ∧ 1 ∈ ℕ ) → ( 𝐹 ‘ 1 ) ∈ dom vol )
70 1 68 69 sylancl ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ dom vol )
71 67 70 eqeltrid ( 𝜑 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ∈ dom vol )
72 65 ineq2d ( 𝑛 = 1 → ( 𝐸 ∩ ( 𝐹𝑛 ) ) = ( 𝐸 ∩ ( 𝐹 ‘ 1 ) ) )
73 72 fveq2d ( 𝑛 = 1 → ( vol* ‘ ( 𝐸 ∩ ( 𝐹𝑛 ) ) ) = ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ 1 ) ) ) )
74 fvex ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ 1 ) ) ) ∈ V
75 73 3 74 fvmpt ( 1 ∈ ℕ → ( 𝐻 ‘ 1 ) = ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ 1 ) ) ) )
76 68 75 ax-mp ( 𝐻 ‘ 1 ) = ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ 1 ) ) )
77 seq1 ( 1 ∈ ℤ → ( seq 1 ( + , 𝐻 ) ‘ 1 ) = ( 𝐻 ‘ 1 ) )
78 60 77 ax-mp ( seq 1 ( + , 𝐻 ) ‘ 1 ) = ( 𝐻 ‘ 1 )
79 67 ineq2i ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) = ( 𝐸 ∩ ( 𝐹 ‘ 1 ) )
80 79 fveq2i ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) ) = ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ 1 ) ) )
81 76 78 80 3eqtr4ri ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 )
82 71 81 jctir ( 𝜑 → ( 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 1 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) ) )
83 peano2nn ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
84 ffvelrn ( ( 𝐹 : ℕ ⟶ dom vol ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ dom vol )
85 1 83 84 syl2an ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ dom vol )
86 unmbl ( ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ dom vol ) → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ dom vol )
87 86 ex ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ dom vol → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ dom vol ) )
88 85 87 syl5com ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ dom vol ) )
89 simpr ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
90 nnuz ℕ = ( ℤ ‘ 1 )
91 89 90 eleqtrdi ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ ‘ 1 ) )
92 fzsuc ( 𝑘 ∈ ( ℤ ‘ 1 ) → ( 1 ... ( 𝑘 + 1 ) ) = ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) )
93 iuneq1 ( ( 1 ... ( 𝑘 + 1 ) ) = ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) → 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) = 𝑛 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) ( 𝐹𝑛 ) )
94 91 92 93 3syl ( ( 𝜑𝑘 ∈ ℕ ) → 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) = 𝑛 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) ( 𝐹𝑛 ) )
95 iunxun 𝑛 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) ( 𝐹𝑛 ) = ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ 𝑛 ∈ { ( 𝑘 + 1 ) } ( 𝐹𝑛 ) )
96 ovex ( 𝑘 + 1 ) ∈ V
97 fveq2 ( 𝑛 = ( 𝑘 + 1 ) → ( 𝐹𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
98 96 97 iunxsn 𝑛 ∈ { ( 𝑘 + 1 ) } ( 𝐹𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) )
99 98 uneq2i ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ 𝑛 ∈ { ( 𝑘 + 1 ) } ( 𝐹𝑛 ) ) = ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
100 95 99 eqtri 𝑛 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) ( 𝐹𝑛 ) = ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
101 94 100 eqtrdi ( ( 𝜑𝑘 ∈ ℕ ) → 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) = ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
102 101 eleq1d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∈ dom vol ↔ ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ dom vol ) )
103 88 102 sylibrd ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol → 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∈ dom vol ) )
104 oveq1 ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) → ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
105 inss1 ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ⊆ 𝐸
106 105 28 sstrid ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ⊆ ℝ )
107 ovolsscl ( ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ⊆ 𝐸𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) ∈ ℝ )
108 105 4 7 107 mp3an2ani ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) ∈ ℝ )
109 mblsplit ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ dom vol ∧ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( ( vol* ‘ ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) + ( vol* ‘ ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
110 85 106 108 109 syl3anc ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( ( vol* ‘ ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) + ( vol* ‘ ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
111 in32 ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∩ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) )
112 inss2 ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) )
113 83 adantl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
114 113 90 eleqtrdi ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ( ℤ ‘ 1 ) )
115 eluzfz2 ( ( 𝑘 + 1 ) ∈ ( ℤ ‘ 1 ) → ( 𝑘 + 1 ) ∈ ( 1 ... ( 𝑘 + 1 ) ) )
116 97 ssiun2s ( ( 𝑘 + 1 ) ∈ ( 1 ... ( 𝑘 + 1 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ⊆ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) )
117 114 115 116 3syl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ⊆ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) )
118 112 117 sstrid ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) )
119 df-ss ( ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ↔ ( ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∩ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) = ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
120 118 119 sylib ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∩ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) = ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
121 111 120 syl5eq ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
122 121 fveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) = ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
123 indif2 ( 𝐸 ∩ ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) = ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
124 uncom ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) )
125 101 124 eqtr2di ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) = 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) )
126 2 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → Disj 𝑖 ∈ ℕ ( 𝐹𝑖 ) )
127 113 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ℕ )
128 16 adantl ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 ∈ ℕ )
129 128 nnred ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 ∈ ℝ )
130 elfzle2 ( 𝑛 ∈ ( 1 ... 𝑘 ) → 𝑛𝑘 )
131 130 adantl ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛𝑘 )
132 89 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑘 ∈ ℕ )
133 nnleltp1 ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑛𝑘𝑛 < ( 𝑘 + 1 ) ) )
134 128 132 133 syl2anc ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝑛𝑘𝑛 < ( 𝑘 + 1 ) ) )
135 131 134 mpbid ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 < ( 𝑘 + 1 ) )
136 129 135 gtned ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝑘 + 1 ) ≠ 𝑛 )
137 fveq2 ( 𝑖 = ( 𝑘 + 1 ) → ( 𝐹𝑖 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
138 fveq2 ( 𝑖 = 𝑛 → ( 𝐹𝑖 ) = ( 𝐹𝑛 ) )
139 137 138 disji2 ( ( Disj 𝑖 ∈ ℕ ( 𝐹𝑖 ) ∧ ( ( 𝑘 + 1 ) ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ≠ 𝑛 ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∩ ( 𝐹𝑛 ) ) = ∅ )
140 126 127 128 136 139 syl121anc ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∩ ( 𝐹𝑛 ) ) = ∅ )
141 140 iuneq2dv ( ( 𝜑𝑘 ∈ ℕ ) → 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∩ ( 𝐹𝑛 ) ) = 𝑛 ∈ ( 1 ... 𝑘 ) ∅ )
142 iunin2 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∩ ( 𝐹𝑛 ) ) = ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∩ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) )
143 iun0 𝑛 ∈ ( 1 ... 𝑘 ) ∅ = ∅
144 141 142 143 3eqtr3g ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∩ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) = ∅ )
145 uneqdifeq ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ⊆ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∩ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) = ∅ ) → ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) = 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ↔ ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) )
146 117 144 145 syl2anc ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) = 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ↔ ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) )
147 125 146 mpbid ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) )
148 147 ineq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐸 ∩ ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) = ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) )
149 123 148 eqtr3id ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) )
150 149 fveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) = ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) )
151 122 150 oveq12d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( vol* ‘ ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) + ( vol* ‘ ( ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ∖ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) = ( ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) + ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ) )
152 inss1 ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ 𝐸
153 ovolsscl ( ( ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ 𝐸𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
154 152 4 7 153 mp3an2ani ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
155 154 recnd ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ℂ )
156 15 recnd ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ∈ ℂ )
157 155 156 addcomd ( ( 𝜑𝑘 ∈ ℕ ) → ( ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) + ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ) = ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
158 110 151 157 3eqtrd ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
159 seqp1 ( 𝑘 ∈ ( ℤ ‘ 1 ) → ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( 𝐻 ‘ ( 𝑘 + 1 ) ) ) )
160 91 159 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( 𝐻 ‘ ( 𝑘 + 1 ) ) ) )
161 97 ineq2d ( 𝑛 = ( 𝑘 + 1 ) → ( 𝐸 ∩ ( 𝐹𝑛 ) ) = ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
162 161 fveq2d ( 𝑛 = ( 𝑘 + 1 ) → ( vol* ‘ ( 𝐸 ∩ ( 𝐹𝑛 ) ) ) = ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
163 fvex ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ∈ V
164 162 3 163 fvmpt ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝐻 ‘ ( 𝑘 + 1 ) ) = ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
165 113 164 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐻 ‘ ( 𝑘 + 1 ) ) = ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
166 165 oveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( 𝐻 ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
167 160 166 eqtrd ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
168 158 167 eqeq12d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) ↔ ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
169 104 168 syl5ibr ( ( 𝜑𝑘 ∈ ℕ ) → ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) ) )
170 103 169 anim12d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ) → ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) ) ) )
171 170 expcom ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ) → ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) ) ) ) )
172 171 a2d ( 𝑘 ∈ ℕ → ( ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ) ) → ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑘 + 1 ) ) ) ) ) )
173 41 50 59 50 82 172 nnind ( 𝑘 ∈ ℕ → ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ) ) )
174 173 impcom ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ) )
175 174 simprd ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) )
176 175 eqcomd ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) = ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) )
177 176 oveq1d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ) = ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ) )
178 174 simpld ( ( 𝜑𝑘 ∈ ℕ ) → 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol )
179 mblsplit ( ( 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ∈ dom vol ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ 𝐸 ) = ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ) )
180 178 28 7 179 syl3anc ( ( 𝜑𝑘 ∈ ℕ ) → ( vol* ‘ 𝐸 ) = ( ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) + ( vol* ‘ ( 𝐸 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹𝑛 ) ) ) ) )
181 32 177 180 3brtr4d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) + ( vol* ‘ ( 𝐸 ran 𝐹 ) ) ) ≤ ( vol* ‘ 𝐸 ) )