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