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

Metamath Proof Explorer

Theorem volsup

Description: The volume of the limit of an increasing sequence of measurable sets is the limit of the volumes. (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion volsup ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ dom vol )
2 1 ad2ant2r ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom vol )
3 fzofi ⊢ ( 1 ..^ 𝑘 ) ∈ Fin
4 simpll ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → 𝐹 : ℕ ⟶ dom vol )
5 elfzouz ⊢ ( 𝑚 ∈ ( 1 ..^ 𝑘 ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) )
6 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
7 5 6 eleqtrrdi ⊢ ( 𝑚 ∈ ( 1 ..^ 𝑘 ) → 𝑚 ∈ ℕ )
8 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∈ dom vol )
9 4 7 8 syl2an ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) ∧ 𝑚 ∈ ( 1 ..^ 𝑘 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ dom vol )
10 9 ralrimiva ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol )
11 finiunmbl ⊢ ( ( ( 1 ..^ 𝑘 ) ∈ Fin ∧ ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol )
12 3 10 11 sylancr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol )
13 difmbl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ dom vol ∧ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol )
14 2 12 13 syl2anc ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol )
15 mblvol ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol* ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) )
16 14 15 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol* ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) )
17 difssd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ⊆ ( 𝐹 ‘ 𝑘 ) )
18 mblss ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ dom vol → ( 𝐹 ‘ 𝑘 ) ⊆ ℝ )
19 2 18 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ⊆ ℝ )
20 mblvol ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ dom vol → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) )
21 2 20 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) )
22 simprr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
23 21 22 eqeltrrd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
24 ovolsscl ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ⊆ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ )
25 17 19 23 24 syl3anc ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ )
26 16 25 eqeltrd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ )
27 14 26 jca ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) )
28 27 expr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) ) )
29 28 ralimdva ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ∀ 𝑘 ∈ ℕ ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) ) )
30 29 imp ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ∀ 𝑘 ∈ ℕ ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) )
31 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
32 31 iundisj2 ⊢ Disj 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) )
33 eqid ⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) )
34 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) )
35 33 34 voliun ⊢ ( ( ∀ 𝑘 ∈ ℕ ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) → ( vol ‘ ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = sup ( ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) , ℝ* , < ) )
36 30 32 35 sylancl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = sup ( ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) , ℝ* , < ) )
37 31 iundisj ⊢ ∪ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) )
38 ffn ⊢ ( 𝐹 : ℕ ⟶ dom vol → 𝐹 Fn ℕ )
39 38 ad2antrr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → 𝐹 Fn ℕ )
40 fniunfv ⊢ ( 𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = ∪ ran 𝐹 )
41 39 40 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ∪ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = ∪ ran 𝐹 )
42 37 41 eqtr3id ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ∪ ran 𝐹 )
43 42 fveq2d ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol ‘ ∪ ran 𝐹 ) )
44 1z ⊢ 1 ∈ ℤ
45 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) )
46 44 45 ax-mp ⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 )
47 6 fneq2i ⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) )
48 46 47 mpbir ⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ℕ
49 48 a1i ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ℕ )
50 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
51 simpll ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → 𝐹 : ℕ ⟶ dom vol )
52 fco ⊢ ( ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℕ ⟶ dom vol ) → ( vol ∘ 𝐹 ) : ℕ ⟶ ( 0 [,] +∞ ) )
53 50 51 52 sylancr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ∘ 𝐹 ) : ℕ ⟶ ( 0 [,] +∞ ) )
54 53 ffnd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ∘ 𝐹 ) Fn ℕ )
55 fveq2 ⊢ ( 𝑥 = 1 → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) )
56 2fveq3 ⊢ ( 𝑥 = 1 → ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) )
57 55 56 eqeq12d ⊢ ( 𝑥 = 1 → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) ) )
58 57 imbi2d ⊢ ( 𝑥 = 1 → ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) ) ) )
59 fveq2 ⊢ ( 𝑥 = 𝑗 → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) )
60 2fveq3 ⊢ ( 𝑥 = 𝑗 → ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) )
61 59 60 eqeq12d ⊢ ( 𝑥 = 𝑗 → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
62 61 imbi2d ⊢ ( 𝑥 = 𝑗 → ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) )
63 fveq2 ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) )
64 2fveq3 ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
65 63 64 eqeq12d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) )
66 65 imbi2d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) )
67 seq1 ⊢ ( 1 ∈ ℤ → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ 1 ) )
68 44 67 ax-mp ⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ 1 )
69 1nn ⊢ 1 ∈ ℕ
70 oveq2 ⊢ ( 𝑘 = 1 → ( 1 ..^ 𝑘 ) = ( 1 ..^ 1 ) )
71 fzo0 ⊢ ( 1 ..^ 1 ) = ∅
72 70 71 eqtrdi ⊢ ( 𝑘 = 1 → ( 1 ..^ 𝑘 ) = ∅ )
73 72 iuneq1d ⊢ ( 𝑘 = 1 → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) = ∪ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) )
74 0iun ⊢ ∪ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) = ∅
75 73 74 eqtrdi ⊢ ( 𝑘 = 1 → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) = ∅ )
76 75 difeq2d ⊢ ( 𝑘 = 1 → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑘 ) ∖ ∅ ) )
77 dif0 ⊢ ( ( 𝐹 ‘ 𝑘 ) ∖ ∅ ) = ( 𝐹 ‘ 𝑘 )
78 76 77 eqtrdi ⊢ ( 𝑘 = 1 → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ( 𝐹 ‘ 𝑘 ) )
79 fveq2 ⊢ ( 𝑘 = 1 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 1 ) )
80 78 79 eqtrd ⊢ ( 𝑘 = 1 → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ( 𝐹 ‘ 1 ) )
81 80 fveq2d ⊢ ( 𝑘 = 1 → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) )
82 fvex ⊢ ( vol ‘ ( 𝐹 ‘ 1 ) ) ∈ V
83 81 34 82 fvmpt ⊢ ( 1 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) )
84 69 83 ax-mp ⊢ ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) )
85 68 84 eqtri ⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) )
86 85 a1i ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) )
87 oveq1 ⊢ ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) )
88 seqp1 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) )
89 88 6 eleq2s ⊢ ( 𝑗 ∈ ℕ → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) )
90 89 adantl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) )
91 undif2 ⊢ ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( ( 𝐹 ‘ 𝑗 ) ∪ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
92 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) )
93 fvoveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
94 92 93 sseq12d ⊢ ( 𝑛 = 𝑗 → ( ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐹 ‘ 𝑗 ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
95 simpllr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
96 simpr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
97 94 95 96 rspcdva ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
98 ssequn1 ⊢ ( ( 𝐹 ‘ 𝑗 ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ↔ ( ( 𝐹 ‘ 𝑗 ) ∪ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
99 97 98 sylib ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ∪ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
100 91 99 eqtr2id ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) = ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) )
101 100 fveq2d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( vol ‘ ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) )
102 simplll ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝐹 : ℕ ⟶ dom vol )
103 102 96 ffvelcdmd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ dom vol )
104 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
105 104 adantl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℕ )
106 102 105 ffvelcdmd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ dom vol )
107 difmbl ⊢ ( ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ dom vol ∧ ( 𝐹 ‘ 𝑗 ) ∈ dom vol ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ∈ dom vol )
108 106 103 107 syl2anc ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ∈ dom vol )
109 disjdif ⊢ ( ( 𝐹 ‘ 𝑗 ) ∩ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ∅
110 109 a1i ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ∩ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ∅ )
111 2fveq3 ⊢ ( 𝑘 = 𝑗 → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) )
112 111 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ) )
113 simplr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
114 112 113 96 rspcdva ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
115 mblvol ⊢ ( ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ∈ dom vol → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( vol* ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) )
116 108 115 syl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( vol* ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) )
117 difssd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
118 mblss ⊢ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ dom vol → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ⊆ ℝ )
119 106 118 syl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ⊆ ℝ )
120 mblvol ⊢ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ dom vol → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( vol* ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
121 106 120 syl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( vol* ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
122 2fveq3 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
123 122 eleq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) )
124 123 113 105 rspcdva ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
125 121 124 eqeltrrd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol* ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
126 ovolsscl ⊢ ( ( ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
127 117 119 125 126 syl3anc ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol* ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
128 116 127 eqeltrd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
129 volun ⊢ ( ( ( ( 𝐹 ‘ 𝑗 ) ∈ dom vol ∧ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ∈ dom vol ∧ ( ( 𝐹 ‘ 𝑗 ) ∩ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ∅ ) ∧ ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ∧ ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) )
130 103 108 110 114 128 129 syl32anc ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) )
131 95 adantr ⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑗 ) ) → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
132 elfznn ⊢ ( 𝑚 ∈ ( 1 ... 𝑗 ) → 𝑚 ∈ ℕ )
133 132 adantl ⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑗 ) ) → 𝑚 ∈ ℕ )
134 elfzuz3 ⊢ ( 𝑚 ∈ ( 1 ... 𝑗 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑚 ) )
135 134 adantl ⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑗 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑚 ) )
136 volsuplem ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑚 ) ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) )
137 131 133 135 136 syl12anc ⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) )
138 137 ralrimiva ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) )
139 iunss ⊢ ( ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) )
140 138 139 sylibr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) )
141 96 6 eleqtrdi ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
142 eluzfz2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) → 𝑗 ∈ ( 1 ... 𝑗 ) )
143 141 142 syl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( 1 ... 𝑗 ) )
144 fveq2 ⊢ ( 𝑚 = 𝑗 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑗 ) )
145 144 ssiun2s ⊢ ( 𝑗 ∈ ( 1 ... 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ⊆ ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) )
146 143 145 syl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ⊆ ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) )
147 140 146 eqssd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑗 ) )
148 96 nnzd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ )
149 fzval3 ⊢ ( 𝑗 ∈ ℤ → ( 1 ... 𝑗 ) = ( 1 ..^ ( 𝑗 + 1 ) ) )
150 148 149 syl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 1 ... 𝑗 ) = ( 1 ..^ ( 𝑗 + 1 ) ) )
151 150 iuneq1d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) = ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) )
152 147 151 eqtr3d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) )
153 152 difeq2d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) )
154 153 fveq2d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) )
155 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
156 oveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 1 ..^ 𝑘 ) = ( 1 ..^ ( 𝑗 + 1 ) ) )
157 156 iuneq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) = ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) )
158 155 157 difeq12d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) )
159 158 fveq2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) )
160 fvex ⊢ ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ V
161 159 34 160 fvmpt ⊢ ( ( 𝑗 + 1 ) ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) )
162 105 161 syl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) )
163 154 162 eqtr4d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) )
164 163 oveq2d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) )
165 101 130 164 3eqtrd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) )
166 90 165 eqeq12d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ↔ ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) ) )
167 87 166 imbitrrid ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) )
168 167 expcom ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) )
169 168 a2d ⊢ ( 𝑗 ∈ ℕ → ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) → ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) )
170 58 62 66 62 86 169 nnind ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
171 170 impcom ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) )
172 fvco3 ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ 𝑗 ∈ ℕ ) → ( ( vol ∘ 𝐹 ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) )
173 51 172 sylan ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( vol ∘ 𝐹 ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) )
174 171 173 eqtr4d ⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( ( vol ∘ 𝐹 ) ‘ 𝑗 ) )
175 49 54 174 eqfnfvd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) = ( vol ∘ 𝐹 ) )
176 175 rneqd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) = ran ( vol ∘ 𝐹 ) )
177 rnco2 ⊢ ran ( vol ∘ 𝐹 ) = ( vol “ ran 𝐹 )
178 176 177 eqtrdi ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) = ( vol “ ran 𝐹 ) )
179 178 supeq1d ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → sup ( ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) , ℝ* , < ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) )
180 36 43 179 3eqtr3d ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) )
181 180 ex ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) )
182 rexnal ⊢ ( ∃ 𝑘 ∈ ℕ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ¬ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
183 fniunfv ⊢ ( 𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 )
184 38 183 syl ⊢ ( 𝐹 : ℕ ⟶ dom vol → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 )
185 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ dom vol )
186 185 ralrimiva ⊢ ( 𝐹 : ℕ ⟶ dom vol → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ dom vol )
187 iunmbl ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ dom vol → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ dom vol )
188 186 187 syl ⊢ ( 𝐹 : ℕ ⟶ dom vol → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ dom vol )
189 184 188 eqeltrrd ⊢ ( 𝐹 : ℕ ⟶ dom vol → ∪ ran 𝐹 ∈ dom vol )
190 189 ad2antrr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ∪ ran 𝐹 ∈ dom vol )
191 mblss ⊢ ( ∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ )
192 190 191 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ∪ ran 𝐹 ⊆ ℝ )
193 ovolcl ⊢ ( ∪ ran 𝐹 ⊆ ℝ → ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* )
194 192 193 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* )
195 pnfge ⊢ ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* → ( vol* ‘ ∪ ran 𝐹 ) ≤ +∞ )
196 194 195 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ ran 𝐹 ) ≤ +∞ )
197 simprr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
198 1 ad2ant2r ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom vol )
199 198 18 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ⊆ ℝ )
200 ovolcl ⊢ ( ( 𝐹 ‘ 𝑘 ) ⊆ ℝ → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* )
201 199 200 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* )
202 xrrebnd ⊢ ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) )
203 201 202 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) )
204 198 20 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) )
205 204 eleq1d ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) )
206 ovolge0 ⊢ ( ( 𝐹 ‘ 𝑘 ) ⊆ ℝ → 0 ≤ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) )
207 mnflt0 ⊢ -∞ < 0
208 mnfxr ⊢ -∞ ∈ ℝ*
209 0xr ⊢ 0 ∈ ℝ*
210 xrltletr ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
211 208 209 210 mp3an12 ⊢ ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* → ( ( -∞ < 0 ∧ 0 ≤ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
212 207 211 mpani ⊢ ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* → ( 0 ≤ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
213 200 206 212 sylc ⊢ ( ( 𝐹 ‘ 𝑘 ) ⊆ ℝ → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) )
214 199 213 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) )
215 214 biantrurd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ↔ ( -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) )
216 203 205 215 3bitr4d ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) )
217 197 216 mtbid ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ¬ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ )
218 nltpnft ⊢ ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) = +∞ ↔ ¬ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) )
219 201 218 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) = +∞ ↔ ¬ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) )
220 217 219 mpbird ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) = +∞ )
221 38 ad2antrr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → 𝐹 Fn ℕ )
222 simprl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → 𝑘 ∈ ℕ )
223 fnfvelrn ⊢ ( ( 𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 )
224 221 222 223 syl2anc ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 )
225 elssuni ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 → ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ran 𝐹 )
226 224 225 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ran 𝐹 )
227 ovolss ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( vol* ‘ ∪ ran 𝐹 ) )
228 226 192 227 syl2anc ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( vol* ‘ ∪ ran 𝐹 ) )
229 220 228 eqbrtrrd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → +∞ ≤ ( vol* ‘ ∪ ran 𝐹 ) )
230 pnfxr ⊢ +∞ ∈ ℝ*
231 xrletri3 ⊢ ( ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ ↔ ( ( vol* ‘ ∪ ran 𝐹 ) ≤ +∞ ∧ +∞ ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
232 194 230 231 sylancl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ ↔ ( ( vol* ‘ ∪ ran 𝐹 ) ≤ +∞ ∧ +∞ ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) )
233 196 229 232 mpbir2and ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ ran 𝐹 ) = +∞ )
234 mblvol ⊢ ( ∪ ran 𝐹 ∈ dom vol → ( vol ‘ ∪ ran 𝐹 ) = ( vol* ‘ ∪ ran 𝐹 ) )
235 190 234 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ∪ ran 𝐹 ) = ( vol* ‘ ∪ ran 𝐹 ) )
236 imassrn ⊢ ( vol “ ran 𝐹 ) ⊆ ran vol
237 frn ⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → ran vol ⊆ ( 0 [,] +∞ ) )
238 50 237 ax-mp ⊢ ran vol ⊆ ( 0 [,] +∞ )
239 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
240 238 239 sstri ⊢ ran vol ⊆ ℝ*
241 236 240 sstri ⊢ ( vol “ ran 𝐹 ) ⊆ ℝ*
242 204 220 eqtrd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = +∞ )
243 simpll ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → 𝐹 : ℕ ⟶ dom vol )
244 ffun ⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → Fun vol )
245 50 244 ax-mp ⊢ Fun vol
246 frn ⊢ ( 𝐹 : ℕ ⟶ dom vol → ran 𝐹 ⊆ dom vol )
247 funfvima2 ⊢ ( ( Fun vol ∧ ran 𝐹 ⊆ dom vol ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( vol “ ran 𝐹 ) ) )
248 245 246 247 sylancr ⊢ ( 𝐹 : ℕ ⟶ dom vol → ( ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( vol “ ran 𝐹 ) ) )
249 243 224 248 sylc ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( vol “ ran 𝐹 ) )
250 242 249 eqeltrrd ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → +∞ ∈ ( vol “ ran 𝐹 ) )
251 supxrpnf ⊢ ( ( ( vol “ ran 𝐹 ) ⊆ ℝ* ∧ +∞ ∈ ( vol “ ran 𝐹 ) ) → sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) = +∞ )
252 241 250 251 sylancr ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) = +∞ )
253 233 235 252 3eqtr4d ⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) )
254 253 rexlimdvaa ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ∃ 𝑘 ∈ ℕ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) )
255 182 254 biimtrrid ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ¬ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) )
256 181 255 pm2.61d ⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) )