MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  volsup Structured version   Visualization version   GIF version

Theorem volsup 23231
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.)
Assertion
Ref Expression
volsup ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
Distinct variable group:   𝑛,𝐹

Proof of Theorem volsup
Dummy variables 𝑗 𝑘 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ffvelrn 6313 . . . . . . . . . . 11 ((𝐹:ℕ⟶dom vol ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ dom vol)
21ad2ant2r 782 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ dom vol)
3 fzofi 12713 . . . . . . . . . . 11 (1..^𝑘) ∈ Fin
4 simpll 789 . . . . . . . . . . . . 13 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
5 elfzouz 12415 . . . . . . . . . . . . . 14 (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ (ℤ‘1))
6 nnuz 11667 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
75, 6syl6eleqr 2709 . . . . . . . . . . . . 13 (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ)
8 ffvelrn 6313 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶dom vol ∧ 𝑚 ∈ ℕ) → (𝐹𝑚) ∈ dom vol)
94, 7, 8syl2an 494 . . . . . . . . . . . 12 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹𝑚) ∈ dom vol)
109ralrimiva 2960 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
11 finiunmbl 23219 . . . . . . . . . . 11 (((1..^𝑘) ∈ Fin ∧ ∀𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
123, 10, 11sylancr 694 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
13 difmbl 23218 . . . . . . . . . 10 (((𝐹𝑘) ∈ dom vol ∧ 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol)
142, 12, 13syl2anc 692 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol)
15 mblvol 23205 . . . . . . . . . . 11 (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
1614, 15syl 17 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
17 difssd 3716 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ⊆ (𝐹𝑘))
18 mblss 23206 . . . . . . . . . . . 12 ((𝐹𝑘) ∈ dom vol → (𝐹𝑘) ⊆ ℝ)
192, 18syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ℝ)
20 mblvol 23205 . . . . . . . . . . . . 13 ((𝐹𝑘) ∈ dom vol → (vol‘(𝐹𝑘)) = (vol*‘(𝐹𝑘)))
212, 20syl 17 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) = (vol*‘(𝐹𝑘)))
22 simprr 795 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) ∈ ℝ)
2321, 22eqeltrrd 2699 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ∈ ℝ)
24 ovolsscl 23161 . . . . . . . . . . 11 ((((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ⊆ (𝐹𝑘) ∧ (𝐹𝑘) ⊆ ℝ ∧ (vol*‘(𝐹𝑘)) ∈ ℝ) → (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2517, 19, 23, 24syl3anc 1323 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2616, 25eqeltrd 2698 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2714, 26jca 554 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ))
2827expr 642 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ 𝑘 ∈ ℕ) → ((vol‘(𝐹𝑘)) ∈ ℝ → (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)))
2928ralimdva 2956 . . . . . 6 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → ∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)))
3029imp 445 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ))
31 fveq2 6148 . . . . . 6 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
3231iundisj2 23224 . . . . 5 Disj 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))
33 eqid 2621 . . . . . 6 seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))
34 eqid 2621 . . . . . 6 (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
3533, 34voliun 23229 . . . . 5 ((∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ) ∧ Disj 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ))
3630, 32, 35sylancl 693 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ))
3731iundisj 23223 . . . . . 6 𝑘 ∈ ℕ (𝐹𝑘) = 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))
38 ffn 6002 . . . . . . . 8 (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
3938ad2antrr 761 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝐹 Fn ℕ)
40 fniunfv 6459 . . . . . . 7 (𝐹 Fn ℕ → 𝑘 ∈ ℕ (𝐹𝑘) = ran 𝐹)
4139, 40syl 17 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝑘 ∈ ℕ (𝐹𝑘) = ran 𝐹)
4237, 41syl5eqr 2669 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ran 𝐹)
4342fveq2d 6152 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘ ran 𝐹))
44 1z 11351 . . . . . . . . . . 11 1 ∈ ℤ
45 seqfn 12753 . . . . . . . . . . 11 (1 ∈ ℤ → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn (ℤ‘1))
4644, 45ax-mp 5 . . . . . . . . . 10 seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn (ℤ‘1)
476fneq2i 5944 . . . . . . . . . 10 (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn ℕ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn (ℤ‘1))
4846, 47mpbir 221 . . . . . . . . 9 seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn ℕ
4948a1i 11 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn ℕ)
50 volf 23204 . . . . . . . . . 10 vol:dom vol⟶(0[,]+∞)
51 simpll 789 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
52 fco 6015 . . . . . . . . . 10 ((vol:dom vol⟶(0[,]+∞) ∧ 𝐹:ℕ⟶dom vol) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
5350, 51, 52sylancr 694 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
54 ffn 6002 . . . . . . . . 9 ((vol ∘ 𝐹):ℕ⟶(0[,]+∞) → (vol ∘ 𝐹) Fn ℕ)
5553, 54syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ)
56 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1))
57 fveq2 6148 . . . . . . . . . . . . . 14 (𝑥 = 1 → (𝐹𝑥) = (𝐹‘1))
5857fveq2d 6152 . . . . . . . . . . . . 13 (𝑥 = 1 → (vol‘(𝐹𝑥)) = (vol‘(𝐹‘1)))
5956, 58eqeq12d 2636 . . . . . . . . . . . 12 (𝑥 = 1 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1))))
6059imbi2d 330 . . . . . . . . . . 11 (𝑥 = 1 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1)))))
61 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗))
62 fveq2 6148 . . . . . . . . . . . . . 14 (𝑥 = 𝑗 → (𝐹𝑥) = (𝐹𝑗))
6362fveq2d 6152 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (vol‘(𝐹𝑥)) = (vol‘(𝐹𝑗)))
6461, 63eqeq12d 2636 . . . . . . . . . . . 12 (𝑥 = 𝑗 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗))))
6564imbi2d 330 . . . . . . . . . . 11 (𝑥 = 𝑗 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)))))
66 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)))
67 fveq2 6148 . . . . . . . . . . . . . 14 (𝑥 = (𝑗 + 1) → (𝐹𝑥) = (𝐹‘(𝑗 + 1)))
6867fveq2d 6152 . . . . . . . . . . . . 13 (𝑥 = (𝑗 + 1) → (vol‘(𝐹𝑥)) = (vol‘(𝐹‘(𝑗 + 1))))
6966, 68eqeq12d 2636 . . . . . . . . . . . 12 (𝑥 = (𝑗 + 1) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
7069imbi2d 330 . . . . . . . . . . 11 (𝑥 = (𝑗 + 1) → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
71 seq1 12754 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1))
7244, 71ax-mp 5 . . . . . . . . . . . . 13 (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1)
73 1nn 10975 . . . . . . . . . . . . . 14 1 ∈ ℕ
74 oveq2 6612 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 1 → (1..^𝑘) = (1..^1))
75 fzo0 12433 . . . . . . . . . . . . . . . . . . . . . 22 (1..^1) = ∅
7674, 75syl6eq 2671 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 1 → (1..^𝑘) = ∅)
7776iuneq1d 4511 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 1 → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = 𝑚 ∈ ∅ (𝐹𝑚))
78 0iun 4543 . . . . . . . . . . . . . . . . . . . 20 𝑚 ∈ ∅ (𝐹𝑚) = ∅
7977, 78syl6eq 2671 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = ∅)
8079difeq2d 3706 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ((𝐹𝑘) ∖ ∅))
81 dif0 3924 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑘) ∖ ∅) = (𝐹𝑘)
8280, 81syl6eq 2671 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = (𝐹𝑘))
83 fveq2 6148 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝐹𝑘) = (𝐹‘1))
8482, 83eqtrd 2655 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = (𝐹‘1))
8584fveq2d 6152 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘(𝐹‘1)))
86 fvex 6158 . . . . . . . . . . . . . . 15 (vol‘(𝐹‘1)) ∈ V
8785, 34, 86fvmpt 6239 . . . . . . . . . . . . . 14 (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1) = (vol‘(𝐹‘1)))
8873, 87ax-mp 5 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1) = (vol‘(𝐹‘1))
8972, 88eqtri 2643 . . . . . . . . . . . 12 (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1))
9089a1i 11 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1)))
91 oveq1 6611 . . . . . . . . . . . . . 14 ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
92 seqp1 12756 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℤ‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
9392, 6eleq2s 2716 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
9493adantl 482 . . . . . . . . . . . . . . 15 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
95 undif2 4016 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1)))
96 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
97 simpllr 798 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)))
98 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (𝐹𝑛) = (𝐹𝑗))
99 oveq1 6611 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1))
10099fveq2d 6152 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
10198, 100sseq12d 3613 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗 → ((𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1))))
102101rspcv 3291 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)) → (𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1))))
10396, 97, 102sylc 65 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1)))
104 ssequn1 3761 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
105103, 104sylib 208 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
10695, 105syl5req 2668 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
107106fveq2d 6152 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
108 simplll 797 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol)
109108, 96ffvelrnd 6316 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ∈ dom vol)
110 peano2nn 10976 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
111110adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
112108, 111ffvelrnd 6316 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol)
113 difmbl 23218 . . . . . . . . . . . . . . . . . 18 (((𝐹‘(𝑗 + 1)) ∈ dom vol ∧ (𝐹𝑗) ∈ dom vol) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol)
114112, 109, 113syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol)
115 disjdif 4012 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅
116115a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅)
117 simplr 791 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ)
118 fveq2 6148 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
119118fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → (vol‘(𝐹𝑘)) = (vol‘(𝐹𝑗)))
120119eleq1d 2683 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol‘(𝐹𝑗)) ∈ ℝ))
121120rspcv 3291 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘(𝐹𝑗)) ∈ ℝ))
12296, 117, 121sylc 65 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹𝑗)) ∈ ℝ)
123 mblvol 23205 . . . . . . . . . . . . . . . . . . 19 (((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
124114, 123syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
125 difssd 3716 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ⊆ (𝐹‘(𝑗 + 1)))
126 mblss 23206 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
127112, 126syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
128 mblvol 23205 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹‘(𝑗 + 1)) ∈ dom vol → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
129112, 128syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
130 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑗 + 1) → (𝐹𝑘) = (𝐹‘(𝑗 + 1)))
131130fveq2d 6152 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 + 1) → (vol‘(𝐹𝑘)) = (vol‘(𝐹‘(𝑗 + 1))))
132131eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 + 1) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
133132rspcv 3291 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 + 1) ∈ ℕ → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
134111, 117, 133sylc 65 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
135129, 134eqeltrrd 2699 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
136 ovolsscl 23161 . . . . . . . . . . . . . . . . . . 19 ((((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ⊆ (𝐹‘(𝑗 + 1)) ∧ (𝐹‘(𝑗 + 1)) ⊆ ℝ ∧ (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
137125, 127, 135, 136syl3anc 1323 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
138124, 137eqeltrd 2698 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
139 volun 23220 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑗) ∈ dom vol ∧ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol ∧ ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅) ∧ ((vol‘(𝐹𝑗)) ∈ ℝ ∧ (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)) → (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
140109, 114, 116, 122, 138, 139syl32anc 1331 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
14197adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)))
142 elfznn 12312 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ)
143142adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ)
144 elfzuz3 12281 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ𝑚))
145144adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ𝑚))
146 volsuplem 23230 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑚))) → (𝐹𝑚) ⊆ (𝐹𝑗))
147141, 143, 145, 146syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹𝑚) ⊆ (𝐹𝑗))
148147ralrimiva 2960 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
149 iunss 4527 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
150148, 149sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
15196, 6syl6eleq 2708 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
152 eluzfz2 12291 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ‘1) → 𝑗 ∈ (1...𝑗))
153151, 152syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗))
154 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑗 → (𝐹𝑚) = (𝐹𝑗))
155154ssiun2s 4530 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (1...𝑗) → (𝐹𝑗) ⊆ 𝑚 ∈ (1...𝑗)(𝐹𝑚))
156153, 155syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ⊆ 𝑚 ∈ (1...𝑗)(𝐹𝑚))
157150, 156eqssd 3600 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) = (𝐹𝑗))
15896nnzd 11425 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
159 fzval3 12477 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℤ → (1...𝑗) = (1..^(𝑗 + 1)))
160158, 159syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1)))
161160iuneq1d 4511 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
162157, 161eqtr3d 2657 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
163162difeq2d 3706 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚)))
164163fveq2d 6152 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
165 oveq2 6612 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1)))
166165iuneq1d 4511 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 + 1) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
167130, 166difeq12d 3707 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑗 + 1) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚)))
168167fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = (𝑗 + 1) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
169 fvex 6158 . . . . . . . . . . . . . . . . . . . 20 (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))) ∈ V
170168, 34, 169fvmpt 6239 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
171111, 170syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
172164, 171eqtr4d 2658 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)))
173172oveq2d 6620 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
174107, 140, 1733eqtrd 2659 . . . . . . . . . . . . . . 15 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
17594, 174eqeq12d 2636 . . . . . . . . . . . . . 14 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))) ↔ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)))))
17691, 175syl5ibr 236 . . . . . . . . . . . . 13 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
177176expcom 451 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
178177a2d 29 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗))) → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
17960, 65, 70, 65, 90, 178nnind 10982 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗))))
180179impcom 446 . . . . . . . . 9 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)))
181 fvco3 6232 . . . . . . . . . 10 ((𝐹:ℕ⟶dom vol ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹𝑗)))
18251, 181sylan 488 . . . . . . . . 9 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹𝑗)))
183180, 182eqtr4d 2658 . . . . . . . 8 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗))
18449, 55, 183eqfnfvd 6270 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = (vol ∘ 𝐹))
185184rneqd 5313 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = ran (vol ∘ 𝐹))
186 rnco2 5601 . . . . . 6 ran (vol ∘ 𝐹) = (vol “ ran 𝐹)
187185, 186syl6eq 2671 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = (vol “ ran 𝐹))
188187supeq1d 8296 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ) = sup((vol “ ran 𝐹), ℝ*, < ))
18936, 43, 1883eqtr3d 2663 . . 3 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
190189ex 450 . 2 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < )))
191 rexnal 2989 . . 3 (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ)
192 fniunfv 6459 . . . . . . . . . . . 12 (𝐹 Fn ℕ → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
19338, 192syl 17 . . . . . . . . . . 11 (𝐹:ℕ⟶dom vol → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
194 ffvelrn 6313 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶dom vol ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ dom vol)
195194ralrimiva 2960 . . . . . . . . . . . 12 (𝐹:ℕ⟶dom vol → ∀𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
196 iunmbl 23228 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol → 𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
197195, 196syl 17 . . . . . . . . . . 11 (𝐹:ℕ⟶dom vol → 𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
198193, 197eqeltrrd 2699 . . . . . . . . . 10 (𝐹:ℕ⟶dom vol → ran 𝐹 ∈ dom vol)
199198ad2antrr 761 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ran 𝐹 ∈ dom vol)
200 mblss 23206 . . . . . . . . 9 ( ran 𝐹 ∈ dom vol → ran 𝐹 ⊆ ℝ)
201199, 200syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ran 𝐹 ⊆ ℝ)
202 ovolcl 23153 . . . . . . . 8 ( ran 𝐹 ⊆ ℝ → (vol*‘ ran 𝐹) ∈ ℝ*)
203201, 202syl 17 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) ∈ ℝ*)
204 pnfge 11908 . . . . . . 7 ((vol*‘ ran 𝐹) ∈ ℝ* → (vol*‘ ran 𝐹) ≤ +∞)
205203, 204syl 17 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) ≤ +∞)
206 simprr 795 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ¬ (vol‘(𝐹𝑘)) ∈ ℝ)
2071ad2ant2r 782 . . . . . . . . . . . . 13 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ dom vol)
208207, 18syl 17 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ℝ)
209 ovolcl 23153 . . . . . . . . . . . 12 ((𝐹𝑘) ⊆ ℝ → (vol*‘(𝐹𝑘)) ∈ ℝ*)
210208, 209syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ∈ ℝ*)
211 xrrebnd 11942 . . . . . . . . . . 11 ((vol*‘(𝐹𝑘)) ∈ ℝ* → ((vol*‘(𝐹𝑘)) ∈ ℝ ↔ (-∞ < (vol*‘(𝐹𝑘)) ∧ (vol*‘(𝐹𝑘)) < +∞)))
212210, 211syl 17 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘(𝐹𝑘)) ∈ ℝ ↔ (-∞ < (vol*‘(𝐹𝑘)) ∧ (vol*‘(𝐹𝑘)) < +∞)))
213207, 20syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) = (vol*‘(𝐹𝑘)))
214213eleq1d 2683 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol*‘(𝐹𝑘)) ∈ ℝ))
215 ovolge0 23156 . . . . . . . . . . . . 13 ((𝐹𝑘) ⊆ ℝ → 0 ≤ (vol*‘(𝐹𝑘)))
216 mnflt0 11903 . . . . . . . . . . . . . 14 -∞ < 0
217 mnfxr 10040 . . . . . . . . . . . . . . 15 -∞ ∈ ℝ*
218 0xr 10030 . . . . . . . . . . . . . . 15 0 ∈ ℝ*
219 xrltletr 11932 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (vol*‘(𝐹𝑘)) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹𝑘))) → -∞ < (vol*‘(𝐹𝑘))))
220217, 218, 219mp3an12 1411 . . . . . . . . . . . . . 14 ((vol*‘(𝐹𝑘)) ∈ ℝ* → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹𝑘))) → -∞ < (vol*‘(𝐹𝑘))))
221216, 220mpani 711 . . . . . . . . . . . . 13 ((vol*‘(𝐹𝑘)) ∈ ℝ* → (0 ≤ (vol*‘(𝐹𝑘)) → -∞ < (vol*‘(𝐹𝑘))))
222209, 215, 221sylc 65 . . . . . . . . . . . 12 ((𝐹𝑘) ⊆ ℝ → -∞ < (vol*‘(𝐹𝑘)))
223208, 222syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → -∞ < (vol*‘(𝐹𝑘)))
224223biantrurd 529 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘(𝐹𝑘)) < +∞ ↔ (-∞ < (vol*‘(𝐹𝑘)) ∧ (vol*‘(𝐹𝑘)) < +∞)))
225212, 214, 2243bitr4d 300 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol*‘(𝐹𝑘)) < +∞))
226206, 225mtbid 314 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ¬ (vol*‘(𝐹𝑘)) < +∞)
227 nltpnft 11939 . . . . . . . . 9 ((vol*‘(𝐹𝑘)) ∈ ℝ* → ((vol*‘(𝐹𝑘)) = +∞ ↔ ¬ (vol*‘(𝐹𝑘)) < +∞))
228210, 227syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘(𝐹𝑘)) = +∞ ↔ ¬ (vol*‘(𝐹𝑘)) < +∞))
229226, 228mpbird 247 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) = +∞)
23038ad2antrr 761 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹 Fn ℕ)
231 simprl 793 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ)
232 fnfvelrn 6312 . . . . . . . . . 10 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ran 𝐹)
233230, 231, 232syl2anc 692 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ ran 𝐹)
234 elssuni 4433 . . . . . . . . 9 ((𝐹𝑘) ∈ ran 𝐹 → (𝐹𝑘) ⊆ ran 𝐹)
235233, 234syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ran 𝐹)
236 ovolss 23160 . . . . . . . 8 (((𝐹𝑘) ⊆ ran 𝐹 ran 𝐹 ⊆ ℝ) → (vol*‘(𝐹𝑘)) ≤ (vol*‘ ran 𝐹))
237235, 201, 236syl2anc 692 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ≤ (vol*‘ ran 𝐹))
238229, 237eqbrtrrd 4637 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → +∞ ≤ (vol*‘ ran 𝐹))
239 pnfxr 10036 . . . . . . 7 +∞ ∈ ℝ*
240 xrletri3 11929 . . . . . . 7 (((vol*‘ ran 𝐹) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((vol*‘ ran 𝐹) = +∞ ↔ ((vol*‘ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol*‘ ran 𝐹))))
241203, 239, 240sylancl 693 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘ ran 𝐹) = +∞ ↔ ((vol*‘ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol*‘ ran 𝐹))))
242205, 238, 241mpbir2and 956 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) = +∞)
243 mblvol 23205 . . . . . 6 ( ran 𝐹 ∈ dom vol → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
244199, 243syl 17 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
245 imassrn 5436 . . . . . . 7 (vol “ ran 𝐹) ⊆ ran vol
246 frn 6010 . . . . . . . . 9 (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
24750, 246ax-mp 5 . . . . . . . 8 ran vol ⊆ (0[,]+∞)
248 iccssxr 12198 . . . . . . . 8 (0[,]+∞) ⊆ ℝ*
249247, 248sstri 3592 . . . . . . 7 ran vol ⊆ ℝ*
250245, 249sstri 3592 . . . . . 6 (vol “ ran 𝐹) ⊆ ℝ*
251213, 229eqtrd 2655 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) = +∞)
252 simpll 789 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
253 ffun 6005 . . . . . . . . . 10 (vol:dom vol⟶(0[,]+∞) → Fun vol)
25450, 253ax-mp 5 . . . . . . . . 9 Fun vol
255 frn 6010 . . . . . . . . 9 (𝐹:ℕ⟶dom vol → ran 𝐹 ⊆ dom vol)
256 funfvima2 6447 . . . . . . . . 9 ((Fun vol ∧ ran 𝐹 ⊆ dom vol) → ((𝐹𝑘) ∈ ran 𝐹 → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹)))
257254, 255, 256sylancr 694 . . . . . . . 8 (𝐹:ℕ⟶dom vol → ((𝐹𝑘) ∈ ran 𝐹 → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹)))
258252, 233, 257sylc 65 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹))
259251, 258eqeltrrd 2699 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → +∞ ∈ (vol “ ran 𝐹))
260 supxrpnf 12091 . . . . . 6 (((vol “ ran 𝐹) ⊆ ℝ* ∧ +∞ ∈ (vol “ ran 𝐹)) → sup((vol “ ran 𝐹), ℝ*, < ) = +∞)
261250, 259, 260sylancr 694 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → sup((vol “ ran 𝐹), ℝ*, < ) = +∞)
262242, 244, 2613eqtr4d 2665 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
263262rexlimdvaa 3025 . . 3 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < )))
264191, 263syl5bir 233 . 2 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (¬ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < )))
265190, 264pm2.61d 170 1 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  cdif 3552  cun 3553  cin 3554  wss 3555  c0 3891   cuni 4402   ciun 4485  Disj wdisj 4583   class class class wbr 4613  cmpt 4673  dom cdm 5074  ran crn 5075  cima 5077  ccom 5078  Fun wfun 5841   Fn wfn 5842  wf 5843  cfv 5847  (class class class)co 6604  Fincfn 7899  supcsup 8290  cr 9879  0cc0 9880  1c1 9881   + caddc 9883  +∞cpnf 10015  -∞cmnf 10016  *cxr 10017   < clt 10018  cle 10019  cn 10964  cz 11321  cuz 11631  [,]cicc 12120  ...cfz 12268  ..^cfzo 12406  seqcseq 12741  vol*covol 23138  volcvol 23139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cc 9201  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-disj 4584  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-z 11322  df-uz 11632  df-q 11733  df-rp 11777  df-xadd 11891  df-ioo 12121  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-rlim 14154  df-sum 14351  df-xmet 19658  df-met 19659  df-ovol 23140  df-vol 23141
This theorem is referenced by:  volsup2  23279  itg1climres  23387  itg2gt0  23433
  Copyright terms: Public domain W3C validator