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

Theorem volsup 25591
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 ffvelcdm 7101 . . . . . . . . . . 11 ((𝐹:ℕ⟶dom vol ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ dom vol)
21ad2ant2r 747 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ dom vol)
3 fzofi 14015 . . . . . . . . . . 11 (1..^𝑘) ∈ Fin
4 simpll 767 . . . . . . . . . . . . 13 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
5 elfzouz 13703 . . . . . . . . . . . . . 14 (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ (ℤ‘1))
6 nnuz 12921 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
75, 6eleqtrrdi 2852 . . . . . . . . . . . . 13 (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ)
8 ffvelcdm 7101 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶dom vol ∧ 𝑚 ∈ ℕ) → (𝐹𝑚) ∈ dom vol)
94, 7, 8syl2an 596 . . . . . . . . . . . 12 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹𝑚) ∈ dom vol)
109ralrimiva 3146 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
11 finiunmbl 25579 . . . . . . . . . . 11 (((1..^𝑘) ∈ Fin ∧ ∀𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
123, 10, 11sylancr 587 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol)
13 difmbl 25578 . . . . . . . . . 10 (((𝐹𝑘) ∈ dom vol ∧ 𝑚 ∈ (1..^𝑘)(𝐹𝑚) ∈ dom vol) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol)
142, 12, 13syl2anc 584 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol)
15 mblvol 25565 . . . . . . . . . . 11 (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
1614, 15syl 17 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
17 difssd 4137 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ⊆ (𝐹𝑘))
18 mblss 25566 . . . . . . . . . . . 12 ((𝐹𝑘) ∈ dom vol → (𝐹𝑘) ⊆ ℝ)
192, 18syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ℝ)
20 mblvol 25565 . . . . . . . . . . . . 13 ((𝐹𝑘) ∈ dom vol → (vol‘(𝐹𝑘)) = (vol*‘(𝐹𝑘)))
212, 20syl 17 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) = (vol*‘(𝐹𝑘)))
22 simprr 773 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) ∈ ℝ)
2321, 22eqeltrrd 2842 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ∈ ℝ)
24 ovolsscl 25521 . . . . . . . . . . 11 ((((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ⊆ (𝐹𝑘) ∧ (𝐹𝑘) ⊆ ℝ ∧ (vol*‘(𝐹𝑘)) ∈ ℝ) → (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2517, 19, 23, 24syl3anc 1373 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2616, 25eqeltrd 2841 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)
2714, 26jca 511 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹𝑘)) ∈ ℝ)) → (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ))
2827expr 456 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ 𝑘 ∈ ℕ) → ((vol‘(𝐹𝑘)) ∈ ℝ → (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)))
2928ralimdva 3167 . . . . . 6 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → ∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ)))
3029imp 406 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ))
31 fveq2 6906 . . . . . 6 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
3231iundisj2 25584 . . . . 5 Disj 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))
33 eqid 2737 . . . . . 6 seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))
34 eqid 2737 . . . . . 6 (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))
3533, 34voliun 25589 . . . . 5 ((∀𝑘 ∈ ℕ (((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) ∈ dom vol ∧ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) ∈ ℝ) ∧ Disj 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ))
3630, 32, 35sylancl 586 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ))
3731iundisj 25583 . . . . . 6 𝑘 ∈ ℕ (𝐹𝑘) = 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))
38 ffn 6736 . . . . . . . 8 (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
3938ad2antrr 726 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝐹 Fn ℕ)
40 fniunfv 7267 . . . . . . 7 (𝐹 Fn ℕ → 𝑘 ∈ ℕ (𝐹𝑘) = ran 𝐹)
4139, 40syl 17 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝑘 ∈ ℕ (𝐹𝑘) = ran 𝐹)
4237, 41eqtr3id 2791 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ran 𝐹)
4342fveq2d 6910 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ 𝑘 ∈ ℕ ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘ ran 𝐹))
44 1z 12647 . . . . . . . . . . 11 1 ∈ ℤ
45 seqfn 14054 . . . . . . . . . . 11 (1 ∈ ℤ → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn (ℤ‘1))
4644, 45ax-mp 5 . . . . . . . . . 10 seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn (ℤ‘1)
476fneq2i 6666 . . . . . . . . . 10 (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn ℕ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn (ℤ‘1))
4846, 47mpbir 231 . . . . . . . . 9 seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn ℕ
4948a1i 11 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) Fn ℕ)
50 volf 25564 . . . . . . . . . 10 vol:dom vol⟶(0[,]+∞)
51 simpll 767 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
52 fco 6760 . . . . . . . . . 10 ((vol:dom vol⟶(0[,]+∞) ∧ 𝐹:ℕ⟶dom vol) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
5350, 51, 52sylancr 587 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞))
5453ffnd 6737 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ)
55 fveq2 6906 . . . . . . . . . . . . 13 (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1))
56 2fveq3 6911 . . . . . . . . . . . . 13 (𝑥 = 1 → (vol‘(𝐹𝑥)) = (vol‘(𝐹‘1)))
5755, 56eqeq12d 2753 . . . . . . . . . . . 12 (𝑥 = 1 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1))))
5857imbi2d 340 . . . . . . . . . . 11 (𝑥 = 1 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1)))))
59 fveq2 6906 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗))
60 2fveq3 6911 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (vol‘(𝐹𝑥)) = (vol‘(𝐹𝑗)))
6159, 60eqeq12d 2753 . . . . . . . . . . . 12 (𝑥 = 𝑗 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗))))
6261imbi2d 340 . . . . . . . . . . 11 (𝑥 = 𝑗 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)))))
63 fveq2 6906 . . . . . . . . . . . . 13 (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)))
64 2fveq3 6911 . . . . . . . . . . . . 13 (𝑥 = (𝑗 + 1) → (vol‘(𝐹𝑥)) = (vol‘(𝐹‘(𝑗 + 1))))
6563, 64eqeq12d 2753 . . . . . . . . . . . 12 (𝑥 = (𝑗 + 1) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
6665imbi2d 340 . . . . . . . . . . 11 (𝑥 = (𝑗 + 1) → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑥) = (vol‘(𝐹𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
67 seq1 14055 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1))
6844, 67ax-mp 5 . . . . . . . . . . . . 13 (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1)
69 1nn 12277 . . . . . . . . . . . . . 14 1 ∈ ℕ
70 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 1 → (1..^𝑘) = (1..^1))
71 fzo0 13723 . . . . . . . . . . . . . . . . . . . . . 22 (1..^1) = ∅
7270, 71eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 1 → (1..^𝑘) = ∅)
7372iuneq1d 5019 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 1 → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = 𝑚 ∈ ∅ (𝐹𝑚))
74 0iun 5063 . . . . . . . . . . . . . . . . . . . 20 𝑚 ∈ ∅ (𝐹𝑚) = ∅
7573, 74eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = ∅)
7675difeq2d 4126 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ((𝐹𝑘) ∖ ∅))
77 dif0 4378 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑘) ∖ ∅) = (𝐹𝑘)
7876, 77eqtrdi 2793 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = (𝐹𝑘))
79 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝐹𝑘) = (𝐹‘1))
8078, 79eqtrd 2777 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = (𝐹‘1))
8180fveq2d 6910 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘(𝐹‘1)))
82 fvex 6919 . . . . . . . . . . . . . . 15 (vol‘(𝐹‘1)) ∈ V
8381, 34, 82fvmpt 7016 . . . . . . . . . . . . . 14 (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1) = (vol‘(𝐹‘1)))
8469, 83ax-mp 5 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘1) = (vol‘(𝐹‘1))
8568, 84eqtri 2765 . . . . . . . . . . . 12 (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1))
8685a1i 11 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘1) = (vol‘(𝐹‘1)))
87 oveq1 7438 . . . . . . . . . . . . . 14 ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
88 seqp1 14057 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℤ‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
8988, 6eleq2s 2859 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
9089adantl 481 . . . . . . . . . . . . . . 15 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
91 undif2 4477 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1)))
92 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗 → (𝐹𝑛) = (𝐹𝑗))
93 fvoveq1 7454 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
9492, 93sseq12d 4017 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → ((𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1))))
95 simpllr 776 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)))
96 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
9794, 95, 96rspcdva 3623 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1)))
98 ssequn1 4186 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
9997, 98sylib 218 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1)))
10091, 99eqtr2id 2790 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
101100fveq2d 6910 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
102 simplll 775 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol)
103102, 96ffvelcdmd 7105 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ∈ dom vol)
104 peano2nn 12278 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
105104adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
106102, 105ffvelcdmd 7105 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol)
107 difmbl 25578 . . . . . . . . . . . . . . . . . 18 (((𝐹‘(𝑗 + 1)) ∈ dom vol ∧ (𝐹𝑗) ∈ dom vol) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol)
108106, 103, 107syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol)
109 disjdif 4472 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅
110109a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅)
111 2fveq3 6911 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → (vol‘(𝐹𝑘)) = (vol‘(𝐹𝑗)))
112111eleq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol‘(𝐹𝑗)) ∈ ℝ))
113 simplr 769 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ)
114112, 113, 96rspcdva 3623 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹𝑗)) ∈ ℝ)
115 mblvol 25565 . . . . . . . . . . . . . . . . . . 19 (((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
116108, 115syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))))
117 difssd 4137 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ⊆ (𝐹‘(𝑗 + 1)))
118 mblss 25566 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
119106, 118syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ)
120 mblvol 25565 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹‘(𝑗 + 1)) ∈ dom vol → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
121106, 120syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1))))
122 2fveq3 6911 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 + 1) → (vol‘(𝐹𝑘)) = (vol‘(𝐹‘(𝑗 + 1))))
123122eleq1d 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑗 + 1) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ))
124123, 113, 105rspcdva 3623 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
125121, 124eqeltrrd 2842 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ)
126 ovolsscl 25521 . . . . . . . . . . . . . . . . . . 19 ((((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ⊆ (𝐹‘(𝑗 + 1)) ∧ (𝐹‘(𝑗 + 1)) ⊆ ℝ ∧ (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
127117, 119, 125, 126syl3anc 1373 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
128116, 127eqeltrd 2841 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)
129 volun 25580 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑗) ∈ dom vol ∧ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) ∈ dom vol ∧ ((𝐹𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ∅) ∧ ((vol‘(𝐹𝑗)) ∈ ℝ ∧ (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) ∈ ℝ)) → (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
130103, 108, 110, 114, 128, 129syl32anc 1380 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))))
13195adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)))
132 elfznn 13593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ)
133132adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ)
134 elfzuz3 13561 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ𝑚))
135134adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ𝑚))
136 volsuplem 25590 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑚))) → (𝐹𝑚) ⊆ (𝐹𝑗))
137131, 133, 135, 136syl12anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹𝑚) ⊆ (𝐹𝑗))
138137ralrimiva 3146 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
139 iunss 5045 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
140138, 139sylibr 234 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) ⊆ (𝐹𝑗))
14196, 6eleqtrdi 2851 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
142 eluzfz2 13572 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ‘1) → 𝑗 ∈ (1...𝑗))
143141, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗))
144 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑗 → (𝐹𝑚) = (𝐹𝑗))
145144ssiun2s 5048 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (1...𝑗) → (𝐹𝑗) ⊆ 𝑚 ∈ (1...𝑗)(𝐹𝑚))
146143, 145syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ⊆ 𝑚 ∈ (1...𝑗)(𝐹𝑚))
147140, 146eqssd 4001 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) = (𝐹𝑗))
14896nnzd 12640 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
149 fzval3 13773 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℤ → (1...𝑗) = (1..^(𝑗 + 1)))
150148, 149syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1)))
151150iuneq1d 5019 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑚 ∈ (1...𝑗)(𝐹𝑚) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
152147, 151eqtr3d 2779 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
153152difeq2d 4126 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚)))
154153fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
155 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 + 1) → (𝐹𝑘) = (𝐹‘(𝑗 + 1)))
156 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1)))
157156iuneq1d 5019 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 + 1) → 𝑚 ∈ (1..^𝑘)(𝐹𝑚) = 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))
158155, 157difeq12d 4127 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑗 + 1) → ((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚)))
159158fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = (𝑗 + 1) → (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
160 fvex 6919 . . . . . . . . . . . . . . . . . . . 20 (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))) ∈ V
161159, 34, 160fvmpt 7016 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
162105, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹𝑚))))
163154, 162eqtr4d 2780 . . . . . . . . . . . . . . . . 17 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)))
164163oveq2d 7447 . . . . . . . . . . . . . . . 16 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹𝑗)))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
165101, 130, 1643eqtrd 2781 . . . . . . . . . . . . . . 15 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))))
16690, 165eqeq12d 2753 . . . . . . . . . . . . . 14 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))) ↔ ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))‘(𝑗 + 1)))))
16787, 166imbitrrid 246 . . . . . . . . . . . . 13 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))
168167expcom 413 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
169168a2d 29 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗))) → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))))
17058, 62, 66, 62, 86, 169nnind 12284 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗))))
171170impcom 407 . . . . . . . . 9 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = (vol‘(𝐹𝑗)))
172 fvco3 7008 . . . . . . . . . 10 ((𝐹:ℕ⟶dom vol ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹𝑗)))
17351, 172sylan 580 . . . . . . . . 9 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹𝑗)))
174171, 173eqtr4d 2780 . . . . . . . 8 ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗))
17549, 54, 174eqfnfvd 7054 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = (vol ∘ 𝐹))
176175rneqd 5949 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = ran (vol ∘ 𝐹))
177 rnco2 6273 . . . . . 6 ran (vol ∘ 𝐹) = (vol “ ran 𝐹)
178176, 177eqtrdi 2793 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))) = (vol “ ran 𝐹))
179178supeq1d 9486 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹𝑘) ∖ 𝑚 ∈ (1..^𝑘)(𝐹𝑚))))), ℝ*, < ) = sup((vol “ ran 𝐹), ℝ*, < ))
18036, 43, 1793eqtr3d 2785 . . 3 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
181180ex 412 . 2 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < )))
182 rexnal 3100 . . 3 (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ)
183 fniunfv 7267 . . . . . . . . . . . 12 (𝐹 Fn ℕ → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
18438, 183syl 17 . . . . . . . . . . 11 (𝐹:ℕ⟶dom vol → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
185 ffvelcdm 7101 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶dom vol ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ dom vol)
186185ralrimiva 3146 . . . . . . . . . . . 12 (𝐹:ℕ⟶dom vol → ∀𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
187 iunmbl 25588 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol → 𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
188186, 187syl 17 . . . . . . . . . . 11 (𝐹:ℕ⟶dom vol → 𝑛 ∈ ℕ (𝐹𝑛) ∈ dom vol)
189184, 188eqeltrrd 2842 . . . . . . . . . 10 (𝐹:ℕ⟶dom vol → ran 𝐹 ∈ dom vol)
190189ad2antrr 726 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ran 𝐹 ∈ dom vol)
191 mblss 25566 . . . . . . . . 9 ( ran 𝐹 ∈ dom vol → ran 𝐹 ⊆ ℝ)
192190, 191syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ran 𝐹 ⊆ ℝ)
193 ovolcl 25513 . . . . . . . 8 ( ran 𝐹 ⊆ ℝ → (vol*‘ ran 𝐹) ∈ ℝ*)
194192, 193syl 17 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) ∈ ℝ*)
195 pnfge 13172 . . . . . . 7 ((vol*‘ ran 𝐹) ∈ ℝ* → (vol*‘ ran 𝐹) ≤ +∞)
196194, 195syl 17 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) ≤ +∞)
197 simprr 773 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ¬ (vol‘(𝐹𝑘)) ∈ ℝ)
1981ad2ant2r 747 . . . . . . . . . . . . 13 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ dom vol)
199198, 18syl 17 . . . . . . . . . . . 12 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ℝ)
200 ovolcl 25513 . . . . . . . . . . . 12 ((𝐹𝑘) ⊆ ℝ → (vol*‘(𝐹𝑘)) ∈ ℝ*)
201199, 200syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ∈ ℝ*)
202 xrrebnd 13210 . . . . . . . . . . 11 ((vol*‘(𝐹𝑘)) ∈ ℝ* → ((vol*‘(𝐹𝑘)) ∈ ℝ ↔ (-∞ < (vol*‘(𝐹𝑘)) ∧ (vol*‘(𝐹𝑘)) < +∞)))
203201, 202syl 17 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘(𝐹𝑘)) ∈ ℝ ↔ (-∞ < (vol*‘(𝐹𝑘)) ∧ (vol*‘(𝐹𝑘)) < +∞)))
204198, 20syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) = (vol*‘(𝐹𝑘)))
205204eleq1d 2826 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol*‘(𝐹𝑘)) ∈ ℝ))
206 ovolge0 25516 . . . . . . . . . . . . 13 ((𝐹𝑘) ⊆ ℝ → 0 ≤ (vol*‘(𝐹𝑘)))
207 mnflt0 13167 . . . . . . . . . . . . . 14 -∞ < 0
208 mnfxr 11318 . . . . . . . . . . . . . . 15 -∞ ∈ ℝ*
209 0xr 11308 . . . . . . . . . . . . . . 15 0 ∈ ℝ*
210 xrltletr 13199 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (vol*‘(𝐹𝑘)) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹𝑘))) → -∞ < (vol*‘(𝐹𝑘))))
211208, 209, 210mp3an12 1453 . . . . . . . . . . . . . 14 ((vol*‘(𝐹𝑘)) ∈ ℝ* → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹𝑘))) → -∞ < (vol*‘(𝐹𝑘))))
212207, 211mpani 696 . . . . . . . . . . . . 13 ((vol*‘(𝐹𝑘)) ∈ ℝ* → (0 ≤ (vol*‘(𝐹𝑘)) → -∞ < (vol*‘(𝐹𝑘))))
213200, 206, 212sylc 65 . . . . . . . . . . . 12 ((𝐹𝑘) ⊆ ℝ → -∞ < (vol*‘(𝐹𝑘)))
214199, 213syl 17 . . . . . . . . . . 11 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → -∞ < (vol*‘(𝐹𝑘)))
215214biantrurd 532 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘(𝐹𝑘)) < +∞ ↔ (-∞ < (vol*‘(𝐹𝑘)) ∧ (vol*‘(𝐹𝑘)) < +∞)))
216203, 205, 2153bitr4d 311 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol‘(𝐹𝑘)) ∈ ℝ ↔ (vol*‘(𝐹𝑘)) < +∞))
217197, 216mtbid 324 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ¬ (vol*‘(𝐹𝑘)) < +∞)
218 nltpnft 13206 . . . . . . . . 9 ((vol*‘(𝐹𝑘)) ∈ ℝ* → ((vol*‘(𝐹𝑘)) = +∞ ↔ ¬ (vol*‘(𝐹𝑘)) < +∞))
219201, 218syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘(𝐹𝑘)) = +∞ ↔ ¬ (vol*‘(𝐹𝑘)) < +∞))
220217, 219mpbird 257 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) = +∞)
22138ad2antrr 726 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹 Fn ℕ)
222 simprl 771 . . . . . . . . . 10 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ)
223 fnfvelrn 7100 . . . . . . . . . 10 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ran 𝐹)
224221, 222, 223syl2anc 584 . . . . . . . . 9 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ∈ ran 𝐹)
225 elssuni 4937 . . . . . . . . 9 ((𝐹𝑘) ∈ ran 𝐹 → (𝐹𝑘) ⊆ ran 𝐹)
226224, 225syl 17 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (𝐹𝑘) ⊆ ran 𝐹)
227 ovolss 25520 . . . . . . . 8 (((𝐹𝑘) ⊆ ran 𝐹 ran 𝐹 ⊆ ℝ) → (vol*‘(𝐹𝑘)) ≤ (vol*‘ ran 𝐹))
228226, 192, 227syl2anc 584 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘(𝐹𝑘)) ≤ (vol*‘ ran 𝐹))
229220, 228eqbrtrrd 5167 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → +∞ ≤ (vol*‘ ran 𝐹))
230 pnfxr 11315 . . . . . . 7 +∞ ∈ ℝ*
231 xrletri3 13196 . . . . . . 7 (((vol*‘ ran 𝐹) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((vol*‘ ran 𝐹) = +∞ ↔ ((vol*‘ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol*‘ ran 𝐹))))
232194, 230, 231sylancl 586 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → ((vol*‘ ran 𝐹) = +∞ ↔ ((vol*‘ ran 𝐹) ≤ +∞ ∧ +∞ ≤ (vol*‘ ran 𝐹))))
233196, 229, 232mpbir2and 713 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol*‘ ran 𝐹) = +∞)
234 mblvol 25565 . . . . . 6 ( ran 𝐹 ∈ dom vol → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
235190, 234syl 17 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
236 imassrn 6089 . . . . . . 7 (vol “ ran 𝐹) ⊆ ran vol
237 frn 6743 . . . . . . . . 9 (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
23850, 237ax-mp 5 . . . . . . . 8 ran vol ⊆ (0[,]+∞)
239 iccssxr 13470 . . . . . . . 8 (0[,]+∞) ⊆ ℝ*
240238, 239sstri 3993 . . . . . . 7 ran vol ⊆ ℝ*
241236, 240sstri 3993 . . . . . 6 (vol “ ran 𝐹) ⊆ ℝ*
242204, 220eqtrd 2777 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) = +∞)
243 simpll 767 . . . . . . . 8 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol)
244 ffun 6739 . . . . . . . . . 10 (vol:dom vol⟶(0[,]+∞) → Fun vol)
24550, 244ax-mp 5 . . . . . . . . 9 Fun vol
246 frn 6743 . . . . . . . . 9 (𝐹:ℕ⟶dom vol → ran 𝐹 ⊆ dom vol)
247 funfvima2 7251 . . . . . . . . 9 ((Fun vol ∧ ran 𝐹 ⊆ dom vol) → ((𝐹𝑘) ∈ ran 𝐹 → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹)))
248245, 246, 247sylancr 587 . . . . . . . 8 (𝐹:ℕ⟶dom vol → ((𝐹𝑘) ∈ ran 𝐹 → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹)))
249243, 224, 248sylc 65 . . . . . . 7 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘(𝐹𝑘)) ∈ (vol “ ran 𝐹))
250242, 249eqeltrrd 2842 . . . . . 6 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → +∞ ∈ (vol “ ran 𝐹))
251 supxrpnf 13360 . . . . . 6 (((vol “ ran 𝐹) ⊆ ℝ* ∧ +∞ ∈ (vol “ ran 𝐹)) → sup((vol “ ran 𝐹), ℝ*, < ) = +∞)
252241, 250, 251sylancr 587 . . . . 5 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → sup((vol “ ran 𝐹), ℝ*, < ) = +∞)
253233, 235, 2523eqtr4d 2787 . . . 4 (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹𝑘)) ∈ ℝ)) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
254253rexlimdvaa 3156 . . 3 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < )))
255182, 254biimtrrid 243 . 2 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (¬ ∀𝑘 ∈ ℕ (vol‘(𝐹𝑘)) ∈ ℝ → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < )))
256181, 255pm2.61d 179 1 ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061  wrex 3070  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333   cuni 4907   ciun 4991  Disj wdisj 5110   class class class wbr 5143  cmpt 5225  dom cdm 5685  ran crn 5686  cima 5688  ccom 5689  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  Fincfn 8985  supcsup 9480  cr 11154  0cc0 11155  1c1 11156   + caddc 11158  +∞cpnf 11292  -∞cmnf 11293  *cxr 11294   < clt 11295  cle 11296  cn 12266  cz 12613  cuz 12878  [,]cicc 13390  ...cfz 13547  ..^cfzo 13694  seqcseq 14042  vol*covol 25497  volcvol 25498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cc 10475  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xadd 13155  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-sum 15723  df-xmet 21357  df-met 21358  df-ovol 25499  df-vol 25500
This theorem is referenced by:  volsup2  25640  itg1climres  25749  itg2gt0  25795
  Copyright terms: Public domain W3C validator