Step | Hyp | Ref
| Expression |
1 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶dom vol ∧
𝑘 ∈ ℕ) →
(𝐹‘𝑘) ∈ dom vol) |
2 | 1 | ad2ant2r 779 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol) |
3 | | fzofi 12635 |
. . . . . . . . . . 11
⊢
(1..^𝑘) ∈
Fin |
4 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol) |
5 | | elfzouz 12343 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈
(ℤ≥‘1)) |
6 | | nnuz 11599 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
7 | 5, 6 | syl6eleqr 2699 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1..^𝑘) → 𝑚 ∈ ℕ) |
8 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶dom vol ∧
𝑚 ∈ ℕ) →
(𝐹‘𝑚) ∈ dom vol) |
9 | 4, 7, 8 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) ∧ 𝑚 ∈ (1..^𝑘)) → (𝐹‘𝑚) ∈ dom vol) |
10 | 9 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∀𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) |
11 | | finiunmbl 23119 |
. . . . . . . . . . 11
⊢
(((1..^𝑘) ∈ Fin
∧ ∀𝑚 ∈
(1..^𝑘)(𝐹‘𝑚) ∈ dom vol) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) |
12 | 3, 10, 11 | sylancr 694 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) |
13 | | difmbl 23118 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑘) ∈ dom vol ∧ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) ∈ dom vol) → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol) |
14 | 2, 12, 13 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol) |
15 | | mblvol 23105 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol*‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) |
17 | | difssd 3700 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘)) |
18 | | mblss 23106 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑘) ∈ dom vol → (𝐹‘𝑘) ⊆ ℝ) |
19 | 2, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ) |
20 | | mblvol 23105 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑘) ∈ dom vol → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘))) |
21 | 2, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘))) |
22 | | simprr 792 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
23 | 21, 22 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈ ℝ) |
24 | | ovolsscl 23061 |
. . . . . . . . . . 11
⊢ ((((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ⊆ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ⊆ ℝ ∧ (vol*‘(𝐹‘𝑘)) ∈ ℝ) → (vol*‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) |
25 | 17, 19, 23, 24 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) →
(vol*‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) |
26 | 16, 25 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) |
27 | 14, 26 | jca 553 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)) |
28 | 27 | expr 641 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ 𝑘 ∈ ℕ) → ((vol‘(𝐹‘𝑘)) ∈ ℝ → (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ))) |
29 | 28 | ralimdva 2945 |
. . . . . 6
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ))) |
30 | 29 | imp 444 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∀𝑘 ∈ ℕ (((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ)) |
31 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) |
32 | 31 | iundisj2 23124 |
. . . . 5
⊢
Disj 𝑘 ∈
ℕ ((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) |
33 | | eqid 2610 |
. . . . . 6
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) |
34 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) = (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))) |
35 | 33, 34 | voliun 23129 |
. . . . 5
⊢
((∀𝑘 ∈
ℕ (((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) ∈ dom vol ∧ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) ∈ ℝ) ∧ Disj 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ*, <
)) |
36 | 30, 32, 35 | sylancl 693 |
. . . 4
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = sup(ran seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ*, <
)) |
37 | 31 | iundisj 23123 |
. . . . . 6
⊢ ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) |
38 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶dom vol →
𝐹 Fn
ℕ) |
39 | 38 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹 Fn ℕ) |
40 | | fniunfv 6409 |
. . . . . . 7
⊢ (𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹) |
41 | 39, 40 | syl 17 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ (𝐹‘𝑘) = ∪ ran 𝐹) |
42 | 37, 41 | syl5eqr 2658 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ∪ ran 𝐹) |
43 | 42 | fveq2d 6107 |
. . . 4
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ 𝑘 ∈ ℕ ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘∪
ran 𝐹)) |
44 | | 1z 11284 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
45 | | seqfn 12675 |
. . . . . . . . . . 11
⊢ (1 ∈
ℤ → seq1( + , (𝑘
∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn
(ℤ≥‘1)) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . . 10
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn
(ℤ≥‘1) |
47 | 6 | fneq2i 5900 |
. . . . . . . . . 10
⊢ (seq1( +
, (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ ↔ seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn
(ℤ≥‘1)) |
48 | 46, 47 | mpbir 220 |
. . . . . . . . 9
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ |
49 | 48 | a1i 11 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) Fn ℕ) |
50 | | volf 23104 |
. . . . . . . . . 10
⊢ vol:dom
vol⟶(0[,]+∞) |
51 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → 𝐹:ℕ⟶dom vol) |
52 | | fco 5971 |
. . . . . . . . . 10
⊢ ((vol:dom
vol⟶(0[,]+∞) ∧ 𝐹:ℕ⟶dom vol) → (vol ∘
𝐹):ℕ⟶(0[,]+∞)) |
53 | 50, 51, 52 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹):ℕ⟶(0[,]+∞)) |
54 | | ffn 5958 |
. . . . . . . . 9
⊢ ((vol
∘ 𝐹):ℕ⟶(0[,]+∞) → (vol
∘ 𝐹) Fn
ℕ) |
55 | 53, 54 | syl 17 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol ∘ 𝐹) Fn ℕ) |
56 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1)) |
57 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) |
58 | 57 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘1))) |
59 | 56, 58 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)))) |
60 | 59 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))))) |
61 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑗 → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗)) |
62 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑗 → (𝐹‘𝑥) = (𝐹‘𝑗)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑗 → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘𝑗))) |
64 | 61, 63 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑗 → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))) |
65 | 64 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑗 → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))))) |
66 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑗 + 1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1))) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑗 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑗 + 1))) |
68 | 67 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑗 + 1) → (vol‘(𝐹‘𝑥)) = (vol‘(𝐹‘(𝑗 + 1)))) |
69 | 66, 68 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥)) ↔ (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))) |
70 | 69 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑗 + 1) → ((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑥) = (vol‘(𝐹‘𝑥))) ↔ (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))) |
71 | | seq1 12676 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1)) |
72 | 44, 71 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (seq1( +
, (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) |
73 | | 1nn 10908 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ |
74 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 1 → (1..^𝑘) = (1..^1)) |
75 | | fzo0 12361 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1..^1) =
∅ |
76 | 74, 75 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 1 → (1..^𝑘) = ∅) |
77 | 76 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ ∅ (𝐹‘𝑚)) |
78 | | 0iun 4513 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑚 ∈ ∅ (𝐹‘𝑚) = ∅ |
79 | 77, 78 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∅) |
80 | 79 | difeq2d 3690 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘𝑘) ∖ ∅)) |
81 | | dif0 3904 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑘) ∖ ∅) = (𝐹‘𝑘) |
82 | 80, 81 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘𝑘)) |
83 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
84 | 82, 83 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = (𝐹‘1)) |
85 | 84 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘(𝐹‘1))) |
86 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(vol‘(𝐹‘1)) ∈ V |
87 | 85, 34, 86 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℕ → ((𝑘 ∈
ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1))) |
88 | 73, 87 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘1) = (vol‘(𝐹‘1)) |
89 | 72, 88 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ (seq1( +
, (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1)) |
90 | 89 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘1) = (vol‘(𝐹‘1))) |
91 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ ((seq1( +
, (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
92 | | seqp1 12678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘1) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
93 | 92, 6 | eleq2s 2706 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → (seq1( +
, (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
94 | 93 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = ((seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
95 | | undif2 3996 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) |
96 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
97 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
98 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗)) |
99 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1)) |
100 | 99 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1))) |
101 | 98, 100 | sseq12d 3597 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)))) |
102 | 101 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ →
(∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) → (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)))) |
103 | 96, 97, 102 | sylc 63 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1))) |
104 | | ssequn1 3745 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑗) ⊆ (𝐹‘(𝑗 + 1)) ↔ ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1))) |
105 | 103, 104 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∪ (𝐹‘(𝑗 + 1))) = (𝐹‘(𝑗 + 1))) |
106 | 95, 105 | syl5req 2657 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) = ((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) |
107 | 106 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))) |
108 | | simplll 794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶dom vol) |
109 | 108, 96 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ dom vol) |
110 | | peano2nn 10909 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ) |
112 | 108, 111 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ∈ dom vol) |
113 | | difmbl 23118 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘(𝑗 + 1)) ∈ dom vol ∧ (𝐹‘𝑗) ∈ dom vol) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol) |
114 | 112, 109,
113 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol) |
115 | | disjdif 3992 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅ |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅) |
117 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ
(vol‘(𝐹‘𝑘)) ∈
ℝ) |
118 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) |
119 | 118 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑗 → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘𝑗))) |
120 | 119 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑗 → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘𝑗)) ∈ ℝ)) |
121 | 120 | rspcv 3278 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ →
(∀𝑘 ∈ ℕ
(vol‘(𝐹‘𝑘)) ∈ ℝ →
(vol‘(𝐹‘𝑗)) ∈
ℝ)) |
122 | 96, 117, 121 | sylc 63 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘𝑗)) ∈ ℝ) |
123 | | mblvol 23105 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) |
124 | 114, 123 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) |
125 | | difssd 3700 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1))) |
126 | | mblss 23106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol → (𝐹‘(𝑗 + 1)) ⊆ ℝ) |
127 | 112, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) ⊆ ℝ) |
128 | | mblvol 23105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘(𝑗 + 1)) ∈ dom vol →
(vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1)))) |
129 | 112, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = (vol*‘(𝐹‘(𝑗 + 1)))) |
130 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1))) |
131 | 130 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝑗 + 1) → (vol‘(𝐹‘𝑘)) = (vol‘(𝐹‘(𝑗 + 1)))) |
132 | 131 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = (𝑗 + 1) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ)) |
133 | 132 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 + 1) ∈ ℕ →
(∀𝑘 ∈ ℕ
(vol‘(𝐹‘𝑘)) ∈ ℝ →
(vol‘(𝐹‘(𝑗 + 1))) ∈
ℝ)) |
134 | 111, 117,
133 | sylc 63 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) ∈ ℝ) |
135 | 129, 134 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ) |
136 | | ovolsscl 23061 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ⊆ (𝐹‘(𝑗 + 1)) ∧ (𝐹‘(𝑗 + 1)) ⊆ ℝ ∧
(vol*‘(𝐹‘(𝑗 + 1))) ∈ ℝ) →
(vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ) |
137 | 125, 127,
135, 136 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol*‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ) |
138 | 124, 137 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ) |
139 | | volun 23120 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑗) ∈ dom vol ∧ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) ∈ dom vol ∧ ((𝐹‘𝑗) ∩ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ∅) ∧ ((vol‘(𝐹‘𝑗)) ∈ ℝ ∧ (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) ∈ ℝ)) →
(vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))) |
140 | 109, 114,
116, 122, 138, 139 | syl32anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘𝑗) ∪ ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))))) |
141 | 97 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
142 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 ∈ (1...𝑗) → 𝑚 ∈ ℕ) |
143 | 142 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑚 ∈ ℕ) |
144 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 ∈ (1...𝑗) → 𝑗 ∈ (ℤ≥‘𝑚)) |
145 | 144 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → 𝑗 ∈ (ℤ≥‘𝑚)) |
146 | | volsuplem 23130 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((∀𝑛 ∈
ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝑚 ∈ ℕ ∧ 𝑗 ∈ (ℤ≥‘𝑚))) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
147 | 141, 143,
145, 146 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑗)) → (𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
148 | 147 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
149 | | iunss 4497 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗) ↔ ∀𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
150 | 148, 149 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) ⊆ (𝐹‘𝑗)) |
151 | 96, 6 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
152 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈
(ℤ≥‘1) → 𝑗 ∈ (1...𝑗)) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (1...𝑗)) |
154 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 𝑗 → (𝐹‘𝑚) = (𝐹‘𝑗)) |
155 | 154 | ssiun2s 4500 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ (1...𝑗) → (𝐹‘𝑗) ⊆ ∪
𝑚 ∈ (1...𝑗)(𝐹‘𝑚)) |
156 | 153, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ⊆ ∪
𝑚 ∈ (1...𝑗)(𝐹‘𝑚)) |
157 | 150, 156 | eqssd 3585 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = (𝐹‘𝑗)) |
158 | 96 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ) |
159 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℤ →
(1...𝑗) = (1..^(𝑗 + 1))) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (1...𝑗) = (1..^(𝑗 + 1))) |
161 | 160 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ∪ 𝑚 ∈ (1...𝑗)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)) |
162 | 157, 161 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)) |
163 | 162 | difeq2d 3690 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) |
164 | 163 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))) |
165 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝑗 + 1) → (1..^𝑘) = (1..^(𝑗 + 1))) |
166 | 165 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = (𝑗 + 1) → ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚) = ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)) |
167 | 130, 166 | difeq12d 3691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)) = ((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) |
168 | 167 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = (𝑗 + 1) → (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))) |
169 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚))) ∈ V |
170 | 168, 34, 169 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))) |
171 | 111, 170 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)) = (vol‘((𝐹‘(𝑗 + 1)) ∖ ∪ 𝑚 ∈ (1..^(𝑗 + 1))(𝐹‘𝑚)))) |
172 | 164, 171 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗))) = ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) |
173 | 172 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol‘(𝐹‘𝑗)) + (vol‘((𝐹‘(𝑗 + 1)) ∖ (𝐹‘𝑗)))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
174 | 107, 140,
173 | 3eqtrd 2648 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (vol‘(𝐹‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1)))) |
175 | 94, 174 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))) ↔ ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))) = ((vol‘(𝐹‘𝑗)) + ((𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))‘(𝑗 + 1))))) |
176 | 91, 175 | syl5ibr 235 |
. . . . . . . . . . . . 13
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1))))) |
177 | 176 | expcom 450 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ((seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)) → (seq1( + , (𝑘 ∈ ℕ ↦ (vol‘((𝐹‘𝑘) ∖ ∪
𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))) |
178 | 177 | a2d 29 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))) → (((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘(𝑗 + 1)) = (vol‘(𝐹‘(𝑗 + 1)))))) |
179 | 60, 65, 70, 65, 90, 178 | nnind 10915 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗)))) |
180 | 179 | impcom 445 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = (vol‘(𝐹‘𝑗))) |
181 | | fvco3 6185 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶dom vol ∧
𝑗 ∈ ℕ) →
((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗))) |
182 | 51, 181 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((vol ∘ 𝐹)‘𝑗) = (vol‘(𝐹‘𝑗))) |
183 | 180, 182 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚)))))‘𝑗) = ((vol ∘ 𝐹)‘𝑗)) |
184 | 49, 55, 183 | eqfnfvd 6222 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → seq1( + , (𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol ∘ 𝐹)) |
185 | 184 | rneqd 5274 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = ran (vol ∘ 𝐹)) |
186 | | rnco2 5559 |
. . . . . 6
⊢ ran (vol
∘ 𝐹) = (vol “
ran 𝐹) |
187 | 185, 186 | syl6eq 2660 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → ran seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))) = (vol “ ran 𝐹)) |
188 | 187 | supeq1d 8235 |
. . . 4
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → sup(ran seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘((𝐹‘𝑘) ∖ ∪ 𝑚 ∈ (1..^𝑘)(𝐹‘𝑚))))), ℝ*, < ) = sup((vol
“ ran 𝐹),
ℝ*, < )) |
189 | 36, 43, 188 | 3eqtr3d 2652 |
. . 3
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ ∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
)) |
190 | 189 | ex 449 |
. 2
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∀𝑘 ∈ ℕ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
))) |
191 | | rexnal 2978 |
. . 3
⊢
(∃𝑘 ∈
ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ ↔ ¬ ∀𝑘 ∈ ℕ
(vol‘(𝐹‘𝑘)) ∈
ℝ) |
192 | | fniunfv 6409 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
193 | 38, 192 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹:ℕ⟶dom vol →
∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
194 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶dom vol ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) ∈ dom vol) |
195 | 194 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝐹:ℕ⟶dom vol →
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ∈ dom vol) |
196 | | iunmbl 23128 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol) |
197 | 195, 196 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹:ℕ⟶dom vol →
∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ dom vol) |
198 | 193, 197 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (𝐹:ℕ⟶dom vol →
∪ ran 𝐹 ∈ dom vol) |
199 | 198 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ∈ dom vol) |
200 | | mblss 23106 |
. . . . . . . . 9
⊢ (∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ) |
201 | 199, 200 | syl 17 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ∪ ran 𝐹 ⊆ ℝ) |
202 | | ovolcl 23053 |
. . . . . . . 8
⊢ (∪ ran 𝐹 ⊆ ℝ → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
203 | 201, 202 | syl 17 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
204 | | pnfge 11840 |
. . . . . . 7
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
(vol*‘∪ ran 𝐹) ≤ +∞) |
205 | 203, 204 | syl 17 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) ≤ +∞) |
206 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ¬
(vol‘(𝐹‘𝑘)) ∈
ℝ) |
207 | 1 | ad2ant2r 779 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ dom vol) |
208 | 207, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ℝ) |
209 | | ovolcl 23053 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑘) ⊆ ℝ → (vol*‘(𝐹‘𝑘)) ∈
ℝ*) |
210 | 208, 209 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ∈
ℝ*) |
211 | | xrrebnd 11873 |
. . . . . . . . . . 11
⊢
((vol*‘(𝐹‘𝑘)) ∈ ℝ* →
((vol*‘(𝐹‘𝑘)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞))) |
212 | 210, 211 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) →
((vol*‘(𝐹‘𝑘)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞))) |
213 | 207, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = (vol*‘(𝐹‘𝑘))) |
214 | 213 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) ∈ ℝ)) |
215 | | ovolge0 23056 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑘) ⊆ ℝ → 0 ≤
(vol*‘(𝐹‘𝑘))) |
216 | | mnflt0 11835 |
. . . . . . . . . . . . . 14
⊢ -∞
< 0 |
217 | | mnfxr 9975 |
. . . . . . . . . . . . . . 15
⊢ -∞
∈ ℝ* |
218 | | 0xr 9965 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ* |
219 | | xrltletr 11864 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘(𝐹‘𝑘)) ∈ ℝ*) →
((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹‘𝑘))) → -∞ < (vol*‘(𝐹‘𝑘)))) |
220 | 217, 218,
219 | mp3an12 1406 |
. . . . . . . . . . . . . 14
⊢
((vol*‘(𝐹‘𝑘)) ∈ ℝ* →
((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐹‘𝑘))) → -∞ < (vol*‘(𝐹‘𝑘)))) |
221 | 216, 220 | mpani 708 |
. . . . . . . . . . . . 13
⊢
((vol*‘(𝐹‘𝑘)) ∈ ℝ* → (0 ≤
(vol*‘(𝐹‘𝑘)) → -∞ <
(vol*‘(𝐹‘𝑘)))) |
222 | 209, 215,
221 | sylc 63 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑘) ⊆ ℝ → -∞ <
(vol*‘(𝐹‘𝑘))) |
223 | 208, 222 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → -∞ <
(vol*‘(𝐹‘𝑘))) |
224 | 223 | biantrurd 528 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) →
((vol*‘(𝐹‘𝑘)) < +∞ ↔
(-∞ < (vol*‘(𝐹‘𝑘)) ∧ (vol*‘(𝐹‘𝑘)) < +∞))) |
225 | 212, 214,
224 | 3bitr4d 299 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol‘(𝐹‘𝑘)) ∈ ℝ ↔ (vol*‘(𝐹‘𝑘)) < +∞)) |
226 | 206, 225 | mtbid 313 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ¬
(vol*‘(𝐹‘𝑘)) <
+∞) |
227 | | nltpnft 11871 |
. . . . . . . . 9
⊢
((vol*‘(𝐹‘𝑘)) ∈ ℝ* →
((vol*‘(𝐹‘𝑘)) = +∞ ↔ ¬
(vol*‘(𝐹‘𝑘)) <
+∞)) |
228 | 210, 227 | syl 17 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) →
((vol*‘(𝐹‘𝑘)) = +∞ ↔ ¬
(vol*‘(𝐹‘𝑘)) <
+∞)) |
229 | 226, 228 | mpbird 246 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) = +∞) |
230 | 38 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹 Fn ℕ) |
231 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝑘 ∈ ℕ) |
232 | | fnfvelrn 6264 |
. . . . . . . . . 10
⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ran 𝐹) |
233 | 230, 231,
232 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ∈ ran 𝐹) |
234 | | elssuni 4403 |
. . . . . . . . 9
⊢ ((𝐹‘𝑘) ∈ ran 𝐹 → (𝐹‘𝑘) ⊆ ∪ ran
𝐹) |
235 | 233, 234 | syl 17 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (𝐹‘𝑘) ⊆ ∪ ran
𝐹) |
236 | | ovolss 23060 |
. . . . . . . 8
⊢ (((𝐹‘𝑘) ⊆ ∪ ran
𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ) → (vol*‘(𝐹‘𝑘)) ≤ (vol*‘∪ ran 𝐹)) |
237 | 235, 201,
236 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘(𝐹‘𝑘)) ≤ (vol*‘∪ ran 𝐹)) |
238 | 229, 237 | eqbrtrrd 4607 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ≤
(vol*‘∪ ran 𝐹)) |
239 | | pnfxr 9971 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
240 | | xrletri3 11861 |
. . . . . . 7
⊢
(((vol*‘∪ ran 𝐹) ∈ ℝ* ∧ +∞
∈ ℝ*) → ((vol*‘∪
ran 𝐹) = +∞ ↔
((vol*‘∪ ran 𝐹) ≤ +∞ ∧ +∞ ≤
(vol*‘∪ ran 𝐹)))) |
241 | 203, 239,
240 | sylancl 693 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → ((vol*‘∪ ran 𝐹) = +∞ ↔ ((vol*‘∪ ran 𝐹) ≤ +∞ ∧ +∞ ≤
(vol*‘∪ ran 𝐹)))) |
242 | 205, 238,
241 | mpbir2and 959 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol*‘∪ ran 𝐹) = +∞) |
243 | | mblvol 23105 |
. . . . . 6
⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
244 | 199, 243 | syl 17 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
245 | | imassrn 5396 |
. . . . . . 7
⊢ (vol
“ ran 𝐹) ⊆ ran
vol |
246 | | frn 5966 |
. . . . . . . . 9
⊢ (vol:dom
vol⟶(0[,]+∞) → ran vol ⊆
(0[,]+∞)) |
247 | 50, 246 | ax-mp 5 |
. . . . . . . 8
⊢ ran vol
⊆ (0[,]+∞) |
248 | | iccssxr 12127 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
249 | 247, 248 | sstri 3577 |
. . . . . . 7
⊢ ran vol
⊆ ℝ* |
250 | 245, 249 | sstri 3577 |
. . . . . 6
⊢ (vol
“ ran 𝐹) ⊆
ℝ* |
251 | 213, 229 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) = +∞) |
252 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → 𝐹:ℕ⟶dom vol) |
253 | | ffun 5961 |
. . . . . . . . . 10
⊢ (vol:dom
vol⟶(0[,]+∞) → Fun vol) |
254 | 50, 253 | ax-mp 5 |
. . . . . . . . 9
⊢ Fun
vol |
255 | | frn 5966 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶dom vol →
ran 𝐹 ⊆ dom
vol) |
256 | | funfvima2 6397 |
. . . . . . . . 9
⊢ ((Fun vol
∧ ran 𝐹 ⊆ dom
vol) → ((𝐹‘𝑘) ∈ ran 𝐹 → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹))) |
257 | 254, 255,
256 | sylancr 694 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶dom vol →
((𝐹‘𝑘) ∈ ran 𝐹 → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹))) |
258 | 252, 233,
257 | sylc 63 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘(𝐹‘𝑘)) ∈ (vol “ ran 𝐹)) |
259 | 251, 258 | eqeltrrd 2689 |
. . . . . 6
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → +∞ ∈
(vol “ ran 𝐹)) |
260 | | supxrpnf 12020 |
. . . . . 6
⊢ (((vol
“ ran 𝐹) ⊆
ℝ* ∧ +∞ ∈ (vol “ ran 𝐹)) → sup((vol “ ran 𝐹), ℝ*, < ) =
+∞) |
261 | 250, 259,
260 | sylancr 694 |
. . . . 5
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → sup((vol “
ran 𝐹),
ℝ*, < ) = +∞) |
262 | 242, 244,
261 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ∧ (𝑘 ∈ ℕ ∧ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ)) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
)) |
263 | 262 | rexlimdvaa 3014 |
. . 3
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (∃𝑘 ∈ ℕ ¬ (vol‘(𝐹‘𝑘)) ∈ ℝ → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
))) |
264 | 191, 263 | syl5bir 232 |
. 2
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (¬ ∀𝑘 ∈ ℕ
(vol‘(𝐹‘𝑘)) ∈ ℝ →
(vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
))) |
265 | 190, 264 | pm2.61d 169 |
1
⊢ ((𝐹:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, <
)) |