| Step | Hyp | Ref
| Expression |
| 1 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶dom vol ∧
𝑘 ∈ ℕ) →
(𝐹‘𝑘) ∈ dom vol) |
| 2 | 1 | ad2ant2r 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) |
| 7 | 5, 6 | eleqtrrdi 2852 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ) |
| 8 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶dom vol ∧
𝑚 ∈ ℕ) →
(𝐹‘𝑚) ∈ dom vol) |
| 9 | 4, 7, 8 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹‘𝑚) ∈ dom vol) |
| 10 | 9 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) |
| 11 | | finiunmbl 25579 |
. . . . . . . . . . 11
⊢
(((1..^𝑘) ∈ Fin
∧ ∀𝑚 ∈
(1..^𝑘)(𝐹‘𝑚) ∈ dom vol) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) |
| 12 | 3, 10, 11 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) |
| 13 | | difmbl 25578 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑘) ∈ dom vol ∧ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol) |
| 14 | 2, 12, 13 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol) |
| 15 | | mblvol 25565 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) |
| 16 | 14, 15 | syl 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 → (𝐹‘𝑘) ⊆ ℝ) |
| 19 | 2, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ) |
| 20 | | mblvol 25565 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑘) ∈ dom vol → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘))) |
| 21 | 2, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘))) |
| 22 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
| 23 | 21, 22 | eqeltrrd 2842 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈ ℝ) |
| 24 | | ovolsscl 25521 |
. . . . . . . . . . 11
⊢ ((((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ⊆ ℝ ∧ (vol*‘(𝐹‘𝑘)) ∈ ℝ) → (vol*‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) |
| 25 | 17, 19, 23, 24 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) →
(vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) |
| 26 | 16, 25 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) |
| 27 | 14, 26 | jca 511 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)) |
| 28 | 27 | expr 456 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ 𝑘 ∈ ℕ) → ((vol‘(𝐹‘𝑘)) ∈ ℝ → (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ))) |
| 29 | 28 | ralimdva 3167 |
. . . . . 6
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ))) |
| 30 | 29 | imp 406 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)) |
| 31 | | fveq2 6906 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) |
| 32 | 31 | iundisj2 25584 |
. . . . 5
⊢
Disj 𝑘 ∈
ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) |
| 33 | | eqid 2737 |
. . . . . 6
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) |
| 34 | | eqid 2737 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) |
| 35 | 33, 34 | voliun 25589 |
. . . . 5
⊢
((∀𝑘 ∈
ℕ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) ∧ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ*, <
)) |
| 36 | 30, 32, 35 | sylancl 586 |
. . . 4
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ*, <
)) |
| 37 | 31 | iundisj 25583 |
. . . . . 6
⊢ ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) |
| 38 | | ffn 6736 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶dom vol →
𝐹 Fn
ℕ) |
| 39 | 38 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹 Fn ℕ) |
| 40 | | fniunfv 7267 |
. . . . . . 7
⊢ (𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹) |
| 41 | 39, 40 | syl 17 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹) |
| 42 | 37, 41 | eqtr3id 2791 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ∪ ran 𝐹) |
| 43 | 42 | fveq2d 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)) |
| 46 | 44, 45 | ax-mp 5 |
. . . . . . . . . 10
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn
(ℤ≥‘1) |
| 47 | 6 | fneq2i 6666 |
. . . . . . . . . 10
⊢ (seq1( +
, (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ ↔ seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn
(ℤ≥‘1)) |
| 48 | 46, 47 | mpbir 231 |
. . . . . . . . 9
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ |
| 49 | 48 | a1i 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[,]+∞)) |
| 53 | 50, 51, 52 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞)) |
| 54 | 53 | ffnd 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))) |
| 57 | 55, 56 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))) |
| 58 | 57 | imbi2d 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‘(𝐹‘𝑗))) |
| 61 | 59, 60 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑗 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))) |
| 62 | 61 | imbi2d 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)))) |
| 65 | 63, 64 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))) |
| 66 | 65 | imbi2d 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)) |
| 68 | 44, 67 | ax-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) =
∅ |
| 72 | 70, 71 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 1 → (1..^𝑘) = ∅) |
| 73 | 72 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ ∅ (𝐹‘𝑚)) |
| 74 | | 0iun 5063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑚 ∈ ∅ (𝐹‘𝑚) = ∅ |
| 75 | 73, 74 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∅) |
| 76 | 75 | difeq2d 4126 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘𝑘) ∖ ∅)) |
| 77 | | dif0 4378 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑘) ∖ ∅) = (𝐹‘𝑘) |
| 78 | 76, 77 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘𝑘)) |
| 79 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
| 80 | 78, 79 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘1)) |
| 81 | 80 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘(𝐹‘1))) |
| 82 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(vol‘(𝐹‘1)) ∈ V |
| 83 | 81, 34, 82 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℕ → ((𝑘 ∈
ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1))) |
| 84 | 69, 83 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1)) |
| 85 | 68, 84 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ (seq1( +
, (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)) |
| 86 | 85 | a1i 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)))) |
| 89 | 88, 6 | eleq2s 2859 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → (seq1( +
, (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
| 90 | 89 | adantl 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))) |
| 94 | 92, 93 | sseq12d 4017 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)))) |
| 95 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
| 96 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
| 97 | 94, 95, 96 | rspcdva 3623 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1))) |
| 98 | | ssequn1 4186 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1))) |
| 99 | 97, 98 | sylib 218 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1))) |
| 100 | 91, 99 | eqtr2id 2790 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) |
| 101 | 100 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))) |
| 102 | | simplll 775 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol) |
| 103 | 102, 96 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ dom vol) |
| 104 | | peano2nn 12278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
| 105 | 104 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ) |
| 106 | 102, 105 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol) |
| 107 | | difmbl 25578 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘(𝑗 + 1)) ∈ dom vol ∧ (𝐹‘𝑗) ∈ dom vol) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol) |
| 108 | 106, 103,
107 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol) |
| 109 | | disjdif 4472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅ |
| 110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅) |
| 111 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑗 → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘𝑗))) |
| 112 | 111 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑗 → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘𝑗)) ∈ ℝ)) |
| 113 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ
(vol‘(𝐹‘𝑘)) ∈
ℝ) |
| 114 | 112, 113,
96 | rspcdva 3623 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘𝑗)) ∈ ℝ) |
| 115 | | mblvol 25565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) |
| 116 | 108, 115 | syl 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)) ⊆ ℝ) |
| 119 | 106, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ) |
| 120 | | mblvol 25565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol →
(vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1)))) |
| 121 | 106, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1)))) |
| 122 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = (𝑗 + 1) → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘(𝑗 + 1)))) |
| 123 | 122 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = (𝑗 + 1) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)) |
| 124 | 123, 113,
105 | rspcdva 3623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ) |
| 125 | 121, 124 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ) |
| 126 | | ovolsscl 25521 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)) ∧ (𝐹‘(𝑗 + 1)) ⊆ ℝ ∧
(vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ) →
(vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ) |
| 127 | 117, 119,
125, 126 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ) |
| 128 | 116, 127 | eqeltrd 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)) ∖ (𝐹‘𝑗))))) |
| 130 | 103, 108,
110, 114, 128, 129 | syl32anc 1380 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))) |
| 131 | 95 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
| 132 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ) |
| 133 | 132 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ) |
| 134 | | elfzuz3 13561 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ≥‘𝑚)) |
| 135 | 134 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ≥‘𝑚)) |
| 136 | | volsuplem 25590 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((∀𝑛 ∈
ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ≥‘𝑚))) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
| 137 | 131, 133,
135, 136 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
| 138 | 137 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
| 139 | | iunss 5045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
| 140 | 138, 139 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
| 141 | 96, 6 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
| 142 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈
(ℤ≥‘1) → 𝑗 ∈ (1...𝑗)) |
| 143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗)) |
| 144 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 𝑗 → (𝐹‘𝑚) = (𝐹‘𝑗)) |
| 145 | 144 | ssiun2s 5048 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ (1...𝑗) → (𝐹‘𝑗) ⊆ ∪
𝑚 ∈ (1...𝑗)(𝐹‘𝑚)) |
| 146 | 143, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ ∪
𝑚 ∈ (1...𝑗)(𝐹‘𝑚)) |
| 147 | 140, 146 | eqssd 4001 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = (𝐹‘𝑗)) |
| 148 | 96 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ) |
| 149 | | fzval3 13773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℤ →
(1...𝑗) = (1..^(𝑗 + 1))) |
| 150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1))) |
| 151 | 150 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)) |
| 152 | 147, 151 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)) |
| 153 | 152 | difeq2d 4126 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) |
| 154 | 153 | fveq2d 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))) |
| 157 | 156 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = (𝑗 + 1) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)) |
| 158 | 155, 157 | difeq12d 4127 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) |
| 159 | 158 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = (𝑗 + 1) → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))) |
| 160 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) ∈ V |
| 161 | 159, 34, 160 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))) |
| 162 | 105, 161 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))) |
| 163 | 154, 162 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) |
| 164 | 163 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
| 165 | 101, 130,
164 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
| 166 | 90, 165 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))) ↔ ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))) |
| 167 | 87, 166 | imbitrrid 246 |
. . . . . . . . . . . . 13
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))) |
| 168 | 167 | expcom 413 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))) |
| 169 | 168 | a2d 29 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))) → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))) |
| 170 | 58, 62, 66, 62, 86, 169 | nnind 12284 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))) |
| 171 | 170 | impcom 407 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))) |
| 172 | | fvco3 7008 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶dom vol ∧
𝑗 ∈ ℕ) →
((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗))) |
| 173 | 51, 172 | sylan 580 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗))) |
| 174 | 171, 173 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗)) |
| 175 | 49, 54, 174 | eqfnfvd 7054 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol ∘ 𝐹)) |
| 176 | 175 | rneqd 5949 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = ran (vol ∘ 𝐹)) |
| 177 | | rnco2 6273 |
. . . . . 6
⊢ ran (vol
∘ 𝐹) = (vol “
ran 𝐹) |
| 178 | 176, 177 | eqtrdi 2793 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol “ ran 𝐹)) |
| 179 | 178 | supeq1d 9486 |
. . . 4
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → sup(ran seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ*, < ) = sup((vol
“ ran 𝐹),
ℝ*, < )) |
| 180 | 36, 43, 179 | 3eqtr3d 2785 |
. . 3
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
)) |
| 181 | 180 | ex 412 |
. 2
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
))) |
| 182 | | rexnal 3100 |
. . 3
⊢
(∃𝑘 ∈
ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ
(vol‘(𝐹‘𝑘)) ∈
ℝ) |
| 183 | | fniunfv 7267 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
| 184 | 38, 183 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹:ℕ⟶dom vol →
∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
| 185 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶dom vol ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) ∈ dom vol) |
| 186 | 185 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝐹:ℕ⟶dom vol →
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ∈ dom vol) |
| 187 | | iunmbl 25588 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol) |
| 188 | 186, 187 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹:ℕ⟶dom vol →
∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol) |
| 189 | 184, 188 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝐹:ℕ⟶dom vol →
∪ ran 𝐹 ∈ dom vol) |
| 190 | 189 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ∈ dom vol) |
| 191 | | mblss 25566 |
. . . . . . . . 9
⊢ (∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ) |
| 192 | 190, 191 | syl 17 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ⊆ ℝ) |
| 193 | | ovolcl 25513 |
. . . . . . . 8
⊢ (∪ ran 𝐹 ⊆ ℝ → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
| 194 | 192, 193 | syl 17 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
| 195 | | pnfge 13172 |
. . . . . . 7
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
(vol*‘∪ ran 𝐹) ≤ +∞) |
| 196 | 194, 195 | syl 17 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) ≤ +∞) |
| 197 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ¬
(vol‘(𝐹‘𝑘)) ∈
ℝ) |
| 198 | 1 | ad2ant2r 747 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol) |
| 199 | 198, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ) |
| 200 | | ovolcl 25513 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑘) ⊆ ℝ → (vol*‘(𝐹‘𝑘)) ∈
ℝ*) |
| 201 | 199, 200 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈
ℝ*) |
| 202 | | xrrebnd 13210 |
. . . . . . . . . . 11
⊢
((vol*‘(𝐹‘𝑘)) ∈ ℝ* →
((vol*‘(𝐹‘𝑘)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞))) |
| 203 | 201, 202 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) →
((vol*‘(𝐹‘𝑘)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞))) |
| 204 | 198, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘))) |
| 205 | 204 | eleq1d 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*‘(𝐹‘𝑘)))) |
| 211 | 208, 209,
210 | mp3an12 1453 |
. . . . . . . . . . . . . 14
⊢
((vol*‘(𝐹‘𝑘)) ∈ ℝ* →
((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹‘𝑘))) → -∞ < (vol*‘(𝐹‘𝑘)))) |
| 212 | 207, 211 | mpani 696 |
. . . . . . . . . . . . 13
⊢
((vol*‘(𝐹‘𝑘)) ∈ ℝ* → (0 ≤
(vol*‘(𝐹‘𝑘)) → -∞ <
(vol*‘(𝐹‘𝑘)))) |
| 213 | 200, 206,
212 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑘) ⊆ ℝ → -∞ <
(vol*‘(𝐹‘𝑘))) |
| 214 | 199, 213 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → -∞ <
(vol*‘(𝐹‘𝑘))) |
| 215 | 214 | biantrurd 532 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) →
((vol*‘(𝐹‘𝑘)) < +∞ ↔
(-∞ < (vol*‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞))) |
| 216 | 203, 205,
215 | 3bitr4d 311 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) < +∞)) |
| 217 | 197, 216 | mtbid 324 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ¬
(vol*‘(𝐹‘𝑘)) <
+∞) |
| 218 | | nltpnft 13206 |
. . . . . . . . 9
⊢
((vol*‘(𝐹‘𝑘)) ∈ ℝ* →
((vol*‘(𝐹‘𝑘)) = +∞ ↔ ¬
(vol*‘(𝐹‘𝑘)) <
+∞)) |
| 219 | 201, 218 | syl 17 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) →
((vol*‘(𝐹‘𝑘)) = +∞ ↔ ¬
(vol*‘(𝐹‘𝑘)) <
+∞)) |
| 220 | 217, 219 | mpbird 257 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) = +∞) |
| 221 | 38 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹 Fn ℕ) |
| 222 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ) |
| 223 | | fnfvelrn 7100 |
. . . . . . . . . 10
⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ran 𝐹) |
| 224 | 221, 222,
223 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ ran 𝐹) |
| 225 | | elssuni 4937 |
. . . . . . . . 9
⊢ ((𝐹‘𝑘) ∈ ran 𝐹 → (𝐹‘𝑘) ⊆ ∪ ran
𝐹) |
| 226 | 224, 225 | syl 17 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ∪ ran
𝐹) |
| 227 | | ovolss 25520 |
. . . . . . . 8
⊢ (((𝐹‘𝑘) ⊆ ∪ ran
𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ) → (vol*‘(𝐹‘𝑘)) ≤ (vol*‘∪ ran 𝐹)) |
| 228 | 226, 192,
227 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ≤ (vol*‘∪ ran 𝐹)) |
| 229 | 220, 228 | eqbrtrrd 5167 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ≤
(vol*‘∪ ran 𝐹)) |
| 230 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 231 | | xrletri3 13196 |
. . . . . . 7
⊢
(((vol*‘∪ ran 𝐹) ∈ ℝ* ∧ +∞
∈ ℝ*) → ((vol*‘∪
ran 𝐹) = +∞ ↔
((vol*‘∪ ran 𝐹) ≤ +∞ ∧ +∞ ≤
(vol*‘∪ ran 𝐹)))) |
| 232 | 194, 230,
231 | sylancl 586 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol*‘∪ ran 𝐹) = +∞ ↔ ((vol*‘∪ ran 𝐹) ≤ +∞ ∧ +∞ ≤
(vol*‘∪ ran 𝐹)))) |
| 233 | 196, 229,
232 | mpbir2and 713 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) = +∞) |
| 234 | | mblvol 25565 |
. . . . . 6
⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
| 235 | 190, 234 | syl 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[,]+∞)) |
| 238 | 50, 237 | ax-mp 5 |
. . . . . . . 8
⊢ ran vol
⊆ (0[,]+∞) |
| 239 | | iccssxr 13470 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
| 240 | 238, 239 | sstri 3993 |
. . . . . . 7
⊢ ran vol
⊆ ℝ* |
| 241 | 236, 240 | sstri 3993 |
. . . . . 6
⊢ (vol
“ ran 𝐹) ⊆
ℝ* |
| 242 | 204, 220 | eqtrd 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) |
| 245 | 50, 244 | ax-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 𝐹))) |
| 248 | 245, 246,
247 | sylancr 587 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶dom vol →
((𝐹‘𝑘) ∈ ran 𝐹 → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹))) |
| 249 | 243, 224,
248 | sylc 65 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹)) |
| 250 | 242, 249 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ∈
(vol “ ran 𝐹)) |
| 251 | | supxrpnf 13360 |
. . . . . 6
⊢ (((vol
“ ran 𝐹) ⊆
ℝ* ∧ +∞ ∈ (vol “ ran 𝐹)) → sup((vol “ ran 𝐹), ℝ*, < ) =
+∞) |
| 252 | 241, 250,
251 | sylancr 587 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → sup((vol “
ran 𝐹),
ℝ*, < ) = +∞) |
| 253 | 233, 235,
252 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
)) |
| 254 | 253 | rexlimdvaa 3156 |
. . 3
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
))) |
| 255 | 182, 254 | biimtrrid 243 |
. 2
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (¬ ∀𝑘 ∈ ℕ
(vol‘(𝐹‘𝑘)) ∈ ℝ →
(vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
))) |
| 256 | 181, 255 | pm2.61d 179 |
1
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
)) |