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 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ 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 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ 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 dfss2 ⊢ ( ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) ↔ ( ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∩ ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) ) = ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
120 118 119 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∩ ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) ) = ( 𝐸 ∩ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
121 111 120 eqtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸 ∩ ∪ 𝑛 ∈ ( 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 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 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* ‘ 𝐸 ) )