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

Theorem volsup 23370
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 6397 . . . . . . . . . . 11 ((𝐹:ℕ⟶dom vol ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ dom vol)
21ad2ant2r 798 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ dom vol)
3 fzofi 12813 . . . . . . . . . . 11 (1..^𝑘) ∈ Fin
4 simpll 805 . . . . . . . . . . . . 13 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
5 elfzouz 12513 . . . . . . . . . . . . . 14 (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ (ℤ‘1))
6 nnuz 11761 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
75, 6syl6eleqr 2741 . . . . . . . . . . . . 13 (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ)
8 ffvelrn 6397 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶dom vol ∧ 𝑚 ∈ ℕ) → (𝐹𝑚) ∈ dom vol)
94, 7, 8syl2an 493 . . . . . . . . . . . 12 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹𝑚) ∈ dom vol)
109ralrimiva 2995 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
11 finiunmbl 23358 . . . . . . . . . . 11 (((1..^𝑘) ∈ Fin ∧ ∀𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
123, 10, 11sylancr 696 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
13 difmbl 23357 . . . . . . . . . 10 (((𝐹𝑘) ∈ dom vol ∧ 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol)
142, 12, 13syl2anc 694 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol)
15 mblvol 23344 . . . . . . . . . . 11 (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
1614, 15syl 17 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
17 difssd 3771 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ⊆ (𝐹𝑘))
18 mblss 23345 . . . . . . . . . . . 12 ((𝐹𝑘) ∈ dom vol → (𝐹𝑘) ⊆ ℝ)
192, 18syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ℝ)
20 mblvol 23344 . . . . . . . . . . . . 13 ((𝐹𝑘) ∈ dom vol → (vol‘(𝐹𝑘)) = (vol*‘(𝐹𝑘)))
212, 20syl 17 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) = (vol*‘(𝐹𝑘)))
22 simprr 811 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) ∈ ℝ)
2321, 22eqeltrrd 2731 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ∈ ℝ)
24 ovolsscl 23300 . . . . . . . . . . 11 ((((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ⊆ (𝐹𝑘) ∧ (𝐹𝑘) ⊆ ℝ ∧ (vol*‘(𝐹𝑘)) ∈ ℝ) → (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2517, 19, 23, 24syl3anc 1366 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2616, 25eqeltrd 2730 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2714, 26jca 553 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ))
2827expr 642 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ 𝑘 ∈ ℕ) → ((vol‘(𝐹𝑘)) ∈ ℝ → (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)))
2928ralimdva 2991 . . . . . 6 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → ∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)))
3029imp 444 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ))
31 fveq2 6229 . . . . . 6 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
3231iundisj2 23363 . . . . 5 Disj 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))
33 eqid 2651 . . . . . 6 seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))
34 eqid 2651 . . . . . 6 (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
3533, 34voliun 23368 . . . . 5 ((∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ) ∧ Disj 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ))
3630, 32, 35sylancl 695 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ))
3731iundisj 23362 . . . . . 6 𝑘 ∈ ℕ (𝐹𝑘) = 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))
38 ffn 6083 . . . . . . . 8 (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
3938ad2antrr 762 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝐹 Fn ℕ)
40 fniunfv 6545 . . . . . . 7 (𝐹 Fn ℕ → 𝑘 ∈ ℕ (𝐹𝑘) = ran 𝐹)
4139, 40syl 17 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝑘 ∈ ℕ (𝐹𝑘) = ran 𝐹)
4237, 41syl5eqr 2699 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ran 𝐹)
4342fveq2d 6233 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘ ran 𝐹))
44 1z 11445 . . . . . . . . . . 11 1 ∈ ℤ
45 seqfn 12853 . . . . . . . . . . 11 (1 ∈ ℤ → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn (ℤ‘1))
4644, 45ax-mp 5 . . . . . . . . . 10 seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn (ℤ‘1)
476fneq2i 6024 . . . . . . . . . 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 23343 . . . . . . . . . 10 vol:dom vol⟶(0[,]+∞)
51 simpll 805 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
52 fco 6096 . . . . . . . . . 10 ((vol:dom vol⟶(0[,]+∞) ∧ 𝐹:ℕ⟶dom vol) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
5350, 51, 52sylancr 696 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
54 ffn 6083 . . . . . . . . 9 ((vol ∘ 𝐹):ℕ⟶(0[,]+∞) → (vol ∘ 𝐹) Fn ℕ)
5553, 54syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ)
56 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1))
57 fveq2 6229 . . . . . . . . . . . . . 14 (𝑥 = 1 → (𝐹𝑥) = (𝐹‘1))
5857fveq2d 6233 . . . . . . . . . . . . 13 (𝑥 = 1 → (vol‘(𝐹𝑥)) = (vol‘(𝐹‘1)))
5956, 58eqeq12d 2666 . . . . . . . . . . . 12 (𝑥 = 1 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1))))
6059imbi2d 329 . . . . . . . . . . 11 (𝑥 = 1 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1)))))
61 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗))
62 fveq2 6229 . . . . . . . . . . . . . 14 (𝑥 = 𝑗 → (𝐹𝑥) = (𝐹𝑗))
6362fveq2d 6233 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (vol‘(𝐹𝑥)) = (vol‘(𝐹𝑗)))
6461, 63eqeq12d 2666 . . . . . . . . . . . 12 (𝑥 = 𝑗 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗))))
6564imbi2d 329 . . . . . . . . . . 11 (𝑥 = 𝑗 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)))))
66 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)))
67 fveq2 6229 . . . . . . . . . . . . . 14 (𝑥 = (𝑗 + 1) → (𝐹𝑥) = (𝐹‘(𝑗 + 1)))
6867fveq2d 6233 . . . . . . . . . . . . 13 (𝑥 = (𝑗 + 1) → (vol‘(𝐹𝑥)) = (vol‘(𝐹‘(𝑗 + 1))))
6966, 68eqeq12d 2666 . . . . . . . . . . . 12 (𝑥 = (𝑗 + 1) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
7069imbi2d 329 . . . . . . . . . . 11 (𝑥 = (𝑗 + 1) → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
71 seq1 12854 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1))
7244, 71ax-mp 5 . . . . . . . . . . . . 13 (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1)
73 1nn 11069 . . . . . . . . . . . . . 14 1 ∈ ℕ
74 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 1 → (1..^𝑘) = (1..^1))
75 fzo0 12531 . . . . . . . . . . . . . . . . . . . . . 22 (1..^1) = ∅
7674, 75syl6eq 2701 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 1 → (1..^𝑘) = ∅)
7776iuneq1d 4577 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 1 → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = 𝑚 ∈ ∅ (𝐹𝑚))
78 0iun 4609 . . . . . . . . . . . . . . . . . . . 20 𝑚 ∈ ∅ (𝐹𝑚) = ∅
7977, 78syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = ∅)
8079difeq2d 3761 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ((𝐹𝑘) ∖ ∅))
81 dif0 3983 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑘) ∖ ∅) = (𝐹𝑘)
8280, 81syl6eq 2701 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = (𝐹𝑘))
83 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝐹𝑘) = (𝐹‘1))
8482, 83eqtrd 2685 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = (𝐹‘1))
8584fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘(𝐹‘1)))
86 fvex 6239 . . . . . . . . . . . . . . 15 (vol‘(𝐹‘1)) ∈ V
8785, 34, 86fvmpt 6321 . . . . . . . . . . . . . 14 (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1) = (vol‘(𝐹‘1)))
8873, 87ax-mp 5 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1) = (vol‘(𝐹‘1))
8972, 88eqtri 2673 . . . . . . . . . . . 12 (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1))
9089a1i 11 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1)))
91 oveq1 6697 . . . . . . . . . . . . . 14 ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
92 seqp1 12856 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℤ‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
9392, 6eleq2s 2748 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
9493adantl 481 . . . . . . . . . . . . . . 15 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
95 undif2 4077 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1)))
96 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
97 simpllr 815 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)))
98 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (𝐹𝑛) = (𝐹𝑗))
99 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1))
10099fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
10198, 100sseq12d 3667 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗 → ((𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1))))
102101rspcv 3336 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)) → (𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1))))
10396, 97, 102sylc 65 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1)))
104 ssequn1 3816 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
105103, 104sylib 208 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
10695, 105syl5req 2698 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
107106fveq2d 6233 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
108 simplll 813 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol)
109108, 96ffvelrnd 6400 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ∈ dom vol)
110 peano2nn 11070 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
111110adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
112108, 111ffvelrnd 6400 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol)
113 difmbl 23357 . . . . . . . . . . . . . . . . . 18 (((𝐹‘(𝑗 + 1)) ∈ dom vol ∧ (𝐹𝑗) ∈ dom vol) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol)
114112, 109, 113syl2anc 694 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol)
115 disjdif 4073 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅
116115a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅)
117 simplr 807 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ)
118 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
119118fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → (vol‘(𝐹𝑘)) = (vol‘(𝐹𝑗)))
120119eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol‘(𝐹𝑗)) ∈ ℝ))
121120rspcv 3336 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘(𝐹𝑗)) ∈ ℝ))
12296, 117, 121sylc 65 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹𝑗)) ∈ ℝ)
123 mblvol 23344 . . . . . . . . . . . . . . . . . . 19 (((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
124114, 123syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
125 difssd 3771 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ⊆ (𝐹‘(𝑗 + 1)))
126 mblss 23345 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
127112, 126syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
128 mblvol 23344 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹‘(𝑗 + 1)) ∈ dom vol → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
129112, 128syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
130 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑗 + 1) → (𝐹𝑘) = (𝐹‘(𝑗 + 1)))
131130fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 + 1) → (vol‘(𝐹𝑘)) = (vol‘(𝐹‘(𝑗 + 1))))
132131eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 + 1) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
133132rspcv 3336 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 + 1) ∈ ℕ → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
134111, 117, 133sylc 65 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
135129, 134eqeltrrd 2731 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
136 ovolsscl 23300 . . . . . . . . . . . . . . . . . . 19 ((((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ⊆ (𝐹‘(𝑗 + 1)) ∧ (𝐹‘(𝑗 + 1)) ⊆ ℝ ∧ (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
137125, 127, 135, 136syl3anc 1366 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
138124, 137eqeltrd 2730 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
139 volun 23359 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑗) ∈ dom vol ∧ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol ∧ ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅) ∧ ((vol‘(𝐹𝑗)) ∈ ℝ ∧ (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)) → (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
140109, 114, 116, 122, 138, 139syl32anc 1374 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
14197adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)))
142 elfznn 12408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ)
143142adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ)
144 elfzuz3 12377 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ𝑚))
145144adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ𝑚))
146 volsuplem 23369 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑚))) → (𝐹𝑚) ⊆ (𝐹𝑗))
147141, 143, 145, 146syl12anc 1364 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹𝑚) ⊆ (𝐹𝑗))
148147ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
149 iunss 4593 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
150148, 149sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
15196, 6syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
152 eluzfz2 12387 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ‘1) → 𝑗 ∈ (1...𝑗))
153151, 152syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗))
154 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑗 → (𝐹𝑚) = (𝐹𝑗))
155154ssiun2s 4596 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (1...𝑗) → (𝐹𝑗) ⊆ 𝑚 ∈ (1...𝑗)(𝐹𝑚))
156153, 155syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ⊆ 𝑚 ∈ (1...𝑗)(𝐹𝑚))
157150, 156eqssd 3653 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) = (𝐹𝑗))
15896nnzd 11519 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
159 fzval3 12576 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℤ → (1...𝑗) = (1..^(𝑗 + 1)))
160158, 159syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1)))
161160iuneq1d 4577 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
162157, 161eqtr3d 2687 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
163162difeq2d 3761 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚)))
164163fveq2d 6233 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
165 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1)))
166165iuneq1d 4577 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 + 1) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
167130, 166difeq12d 3762 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑗 + 1) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚)))
168167fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = (𝑗 + 1) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
169 fvex 6239 . . . . . . . . . . . . . . . . . . . 20 (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))) ∈ V
170168, 34, 169fvmpt 6321 . . . . . . . . . . . . . . . . . . 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 2688 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)))
173172oveq2d 6706 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
174107, 140, 1733eqtrd 2689 . . . . . . . . . . . . . . 15 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
17594, 174eqeq12d 2666 . . . . . . . . . . . . . 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 450 . . . . . . . . . . . 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 11076 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗))))
180179impcom 445 . . . . . . . . 9 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)))
181 fvco3 6314 . . . . . . . . . 10 ((𝐹:ℕ⟶dom vol ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹𝑗)))
18251, 181sylan 487 . . . . . . . . 9 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹𝑗)))
183180, 182eqtr4d 2688 . . . . . . . 8 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗))
18449, 55, 183eqfnfvd 6354 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = (vol ∘ 𝐹))
185184rneqd 5385 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = ran (vol ∘ 𝐹))
186 rnco2 5680 . . . . . 6 ran (vol ∘ 𝐹) = (vol “ ran 𝐹)
187185, 186syl6eq 2701 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = (vol “ ran 𝐹))
188187supeq1d 8393 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ) = sup((vol “ ran 𝐹), ℝ*, < ))
18936, 43, 1883eqtr3d 2693 . . 3 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
190189ex 449 . 2 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < )))
191 rexnal 3024 . . 3 (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ)
192 fniunfv 6545 . . . . . . . . . . . 12 (𝐹 Fn ℕ → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
19338, 192syl 17 . . . . . . . . . . 11 (𝐹:ℕ⟶dom vol → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
194 ffvelrn 6397 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶dom vol ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ dom vol)
195194ralrimiva 2995 . . . . . . . . . . . 12 (𝐹:ℕ⟶dom vol → ∀𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
196 iunmbl 23367 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol → 𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
197195, 196syl 17 . . . . . . . . . . 11 (𝐹:ℕ⟶dom vol → 𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
198193, 197eqeltrrd 2731 . . . . . . . . . 10 (𝐹:ℕ⟶dom vol → ran 𝐹 ∈ dom vol)
199198ad2antrr 762 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ran 𝐹 ∈ dom vol)
200 mblss 23345 . . . . . . . . 9 ( ran 𝐹 ∈ dom vol → ran 𝐹 ⊆ ℝ)
201199, 200syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ran 𝐹 ⊆ ℝ)
202 ovolcl 23292 . . . . . . . 8 ( ran 𝐹 ⊆ ℝ → (vol*‘ ran 𝐹) ∈ ℝ*)
203201, 202syl 17 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) ∈ ℝ*)
204 pnfge 12002 . . . . . . 7 ((vol*‘ ran 𝐹) ∈ ℝ* → (vol*‘ ran 𝐹) ≤ +∞)
205203, 204syl 17 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) ≤ +∞)
206 simprr 811 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ¬ (vol‘(𝐹𝑘)) ∈ ℝ)
2071ad2ant2r 798 . . . . . . . . . . . . 13 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ dom vol)
208207, 18syl 17 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ℝ)
209 ovolcl 23292 . . . . . . . . . . . 12 ((𝐹𝑘) ⊆ ℝ → (vol*‘(𝐹𝑘)) ∈ ℝ*)
210208, 209syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ∈ ℝ*)
211 xrrebnd 12037 . . . . . . . . . . 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 2715 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol*‘(𝐹𝑘)) ∈ ℝ))
215 ovolge0 23295 . . . . . . . . . . . . 13 ((𝐹𝑘) ⊆ ℝ → 0 ≤ (vol*‘(𝐹𝑘)))
216 mnflt0 11997 . . . . . . . . . . . . . 14 -∞ < 0
217 mnfxr 10134 . . . . . . . . . . . . . . 15 -∞ ∈ ℝ*
218 0xr 10124 . . . . . . . . . . . . . . 15 0 ∈ ℝ*
219 xrltletr 12026 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (vol*‘(𝐹𝑘)) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹𝑘))) → -∞ < (vol*‘(𝐹𝑘))))
220217, 218, 219mp3an12 1454 . . . . . . . . . . . . . 14 ((vol*‘(𝐹𝑘)) ∈ ℝ* → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹𝑘))) → -∞ < (vol*‘(𝐹𝑘))))
221216, 220mpani 712 . . . . . . . . . . . . 13 ((vol*‘(𝐹𝑘)) ∈ ℝ* → (0 ≤ (vol*‘(𝐹𝑘)) → -∞ < (vol*‘(𝐹𝑘))))
222209, 215, 221sylc 65 . . . . . . . . . . . 12 ((𝐹𝑘) ⊆ ℝ → -∞ < (vol*‘(𝐹𝑘)))
223208, 222syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → -∞ < (vol*‘(𝐹𝑘)))
224223biantrurd 528 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘(𝐹𝑘)) < +∞ ↔ (-∞ < (vol*‘(𝐹𝑘)) ∧ (vol*‘(𝐹𝑘)) < +∞)))
225212, 214, 2243bitr4d 300 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol*‘(𝐹𝑘)) < +∞))
226206, 225mtbid 313 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ¬ (vol*‘(𝐹𝑘)) < +∞)
227 nltpnft 12033 . . . . . . . . 9 ((vol*‘(𝐹𝑘)) ∈ ℝ* → ((vol*‘(𝐹𝑘)) = +∞ ↔ ¬ (vol*‘(𝐹𝑘)) < +∞))
228210, 227syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘(𝐹𝑘)) = +∞ ↔ ¬ (vol*‘(𝐹𝑘)) < +∞))
229226, 228mpbird 247 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) = +∞)
23038ad2antrr 762 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹 Fn ℕ)
231 simprl 809 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ)
232 fnfvelrn 6396 . . . . . . . . . 10 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ran 𝐹)
233230, 231, 232syl2anc 694 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ ran 𝐹)
234 elssuni 4499 . . . . . . . . 9 ((𝐹𝑘) ∈ ran 𝐹 → (𝐹𝑘) ⊆ ran 𝐹)
235233, 234syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ran 𝐹)
236 ovolss 23299 . . . . . . . 8 (((𝐹𝑘) ⊆ ran 𝐹 ran 𝐹 ⊆ ℝ) → (vol*‘(𝐹𝑘)) ≤ (vol*‘ ran 𝐹))
237235, 201, 236syl2anc 694 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ≤ (vol*‘ ran 𝐹))
238229, 237eqbrtrrd 4709 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → +∞ ≤ (vol*‘ ran 𝐹))
239 pnfxr 10130 . . . . . . 7 +∞ ∈ ℝ*
240 xrletri3 12023 . . . . . . 7 (((vol*‘ ran 𝐹) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((vol*‘ ran 𝐹) = +∞ ↔ ((vol*‘ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol*‘ ran 𝐹))))
241203, 239, 240sylancl 695 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘ ran 𝐹) = +∞ ↔ ((vol*‘ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol*‘ ran 𝐹))))
242205, 238, 241mpbir2and 977 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) = +∞)
243 mblvol 23344 . . . . . 6 ( ran 𝐹 ∈ dom vol → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
244199, 243syl 17 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
245 imassrn 5512 . . . . . . 7 (vol “ ran 𝐹) ⊆ ran vol
246 frn 6091 . . . . . . . . 9 (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
24750, 246ax-mp 5 . . . . . . . 8 ran vol ⊆ (0[,]+∞)
248 iccssxr 12294 . . . . . . . 8 (0[,]+∞) ⊆ ℝ*
249247, 248sstri 3645 . . . . . . 7 ran vol ⊆ ℝ*
250245, 249sstri 3645 . . . . . 6 (vol “ ran 𝐹) ⊆ ℝ*
251213, 229eqtrd 2685 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) = +∞)
252 simpll 805 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
253 ffun 6086 . . . . . . . . . 10 (vol:dom vol⟶(0[,]+∞) → Fun vol)
25450, 253ax-mp 5 . . . . . . . . 9 Fun vol
255 frn 6091 . . . . . . . . 9 (𝐹:ℕ⟶dom vol → ran 𝐹 ⊆ dom vol)
256 funfvima2 6533 . . . . . . . . 9 ((Fun vol ∧ ran 𝐹 ⊆ dom vol) → ((𝐹𝑘) ∈ ran 𝐹 → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹)))
257254, 255, 256sylancr 696 . . . . . . . 8 (𝐹:ℕ⟶dom vol → ((𝐹𝑘) ∈ ran 𝐹 → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹)))
258252, 233, 257sylc 65 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹))
259251, 258eqeltrrd 2731 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → +∞ ∈ (vol “ ran 𝐹))
260 supxrpnf 12186 . . . . . 6 (((vol “ ran 𝐹) ⊆ ℝ* ∧ +∞ ∈ (vol “ ran 𝐹)) → sup((vol “ ran 𝐹), ℝ*, < ) = +∞)
261250, 259, 260sylancr 696 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → sup((vol “ ran 𝐹), ℝ*, < ) = +∞)
262242, 244, 2613eqtr4d 2695 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
263262rexlimdvaa 3061 . . 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 383   = wceq 1523  wcel 2030  wral 2941  wrex 2942  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948   cuni 4468   ciun 4552  Disj wdisj 4652   class class class wbr 4685  cmpt 4762  dom cdm 5143  ran crn 5144  cima 5146  ccom 5147  Fun wfun 5920   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  Fincfn 7997  supcsup 8387  cr 9973  0cc0 9974  1c1 9975   + caddc 9977  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111   < clt 10112  cle 10113  cn 11058  cz 11415  cuz 11725  [,]cicc 12216  ...cfz 12364  ..^cfzo 12504  seqcseq 12841  vol*covol 23277  volcvol 23278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cc 9295  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xadd 11985  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-xmet 19787  df-met 19788  df-ovol 23279  df-vol 23280
This theorem is referenced by:  volsup2  23419  itg1climres  23526  itg2gt0  23572
  Copyright terms: Public domain W3C validator