| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ dom vol ) |
| 2 |
1
|
ad2ant2r |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom vol ) |
| 3 |
|
fzofi |
⊢ ( 1 ..^ 𝑘 ) ∈ Fin |
| 4 |
|
simpll |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → 𝐹 : ℕ ⟶ dom vol ) |
| 5 |
|
elfzouz |
⊢ ( 𝑚 ∈ ( 1 ..^ 𝑘 ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) ) |
| 6 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
| 7 |
5 6
|
eleqtrrdi |
⊢ ( 𝑚 ∈ ( 1 ..^ 𝑘 ) → 𝑚 ∈ ℕ ) |
| 8 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) |
| 9 |
4 7 8
|
syl2an |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) ∧ 𝑚 ∈ ( 1 ..^ 𝑘 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) |
| 10 |
9
|
ralrimiva |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) |
| 11 |
|
finiunmbl |
⊢ ( ( ( 1 ..^ 𝑘 ) ∈ Fin ∧ ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) |
| 12 |
3 10 11
|
sylancr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) |
| 13 |
|
difmbl |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ dom vol ∧ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ∈ dom vol ) → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ) |
| 14 |
2 12 13
|
syl2anc |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ) |
| 15 |
|
mblvol |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol* ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) |
| 16 |
14 15
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol* ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) |
| 17 |
|
difssd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ⊆ ( 𝐹 ‘ 𝑘 ) ) |
| 18 |
|
mblss |
⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ dom vol → ( 𝐹 ‘ 𝑘 ) ⊆ ℝ ) |
| 19 |
2 18
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ⊆ ℝ ) |
| 20 |
|
mblvol |
⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ dom vol → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
| 21 |
2 20
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
| 22 |
|
simprr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) |
| 23 |
21 22
|
eqeltrrd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) |
| 24 |
|
ovolsscl |
⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ⊆ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) |
| 25 |
17 19 23 24
|
syl3anc |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) |
| 26 |
16 25
|
eqeltrd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) |
| 27 |
14 26
|
jca |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) ) |
| 28 |
27
|
expr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) ) ) |
| 29 |
28
|
ralimdva |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ∀ 𝑘 ∈ ℕ ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) ) ) |
| 30 |
29
|
imp |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ∀ 𝑘 ∈ ℕ ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) ) |
| 31 |
|
fveq2 |
⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) ) |
| 32 |
31
|
iundisj2 |
⊢ Disj 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) |
| 33 |
|
eqid |
⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) |
| 34 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) |
| 35 |
33 34
|
voliun |
⊢ ( ( ∀ 𝑘 ∈ ℕ ( ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ ) ∧ Disj 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) → ( vol ‘ ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = sup ( ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) , ℝ* , < ) ) |
| 36 |
30 32 35
|
sylancl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = sup ( ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) , ℝ* , < ) ) |
| 37 |
31
|
iundisj |
⊢ ∪ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) |
| 38 |
|
ffn |
⊢ ( 𝐹 : ℕ ⟶ dom vol → 𝐹 Fn ℕ ) |
| 39 |
38
|
ad2antrr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → 𝐹 Fn ℕ ) |
| 40 |
|
fniunfv |
⊢ ( 𝐹 Fn ℕ → ∪ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = ∪ ran 𝐹 ) |
| 41 |
39 40
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ∪ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = ∪ ran 𝐹 ) |
| 42 |
37 41
|
eqtr3id |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ∪ ran 𝐹 ) |
| 43 |
42
|
fveq2d |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ∪ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol ‘ ∪ ran 𝐹 ) ) |
| 44 |
|
1z |
⊢ 1 ∈ ℤ |
| 45 |
|
seqfn |
⊢ ( 1 ∈ ℤ → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) ) |
| 46 |
44 45
|
ax-mp |
⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) |
| 47 |
6
|
fneq2i |
⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) ) |
| 48 |
46 47
|
mpbir |
⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ℕ |
| 49 |
48
|
a1i |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) Fn ℕ ) |
| 50 |
|
volf |
⊢ vol : dom vol ⟶ ( 0 [,] +∞ ) |
| 51 |
|
simpll |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → 𝐹 : ℕ ⟶ dom vol ) |
| 52 |
|
fco |
⊢ ( ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℕ ⟶ dom vol ) → ( vol ∘ 𝐹 ) : ℕ ⟶ ( 0 [,] +∞ ) ) |
| 53 |
50 51 52
|
sylancr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ∘ 𝐹 ) : ℕ ⟶ ( 0 [,] +∞ ) ) |
| 54 |
53
|
ffnd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ∘ 𝐹 ) Fn ℕ ) |
| 55 |
|
fveq2 |
⊢ ( 𝑥 = 1 → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) ) |
| 56 |
|
2fveq3 |
⊢ ( 𝑥 = 1 → ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) ) |
| 57 |
55 56
|
eqeq12d |
⊢ ( 𝑥 = 1 → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) ) ) |
| 58 |
57
|
imbi2d |
⊢ ( 𝑥 = 1 → ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) ) ) ) |
| 59 |
|
fveq2 |
⊢ ( 𝑥 = 𝑗 → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) ) |
| 60 |
|
2fveq3 |
⊢ ( 𝑥 = 𝑗 → ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) |
| 61 |
59 60
|
eqeq12d |
⊢ ( 𝑥 = 𝑗 → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) |
| 62 |
61
|
imbi2d |
⊢ ( 𝑥 = 𝑗 → ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ) |
| 63 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) |
| 64 |
|
2fveq3 |
⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) |
| 65 |
63 64
|
eqeq12d |
⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) |
| 66 |
65
|
imbi2d |
⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑥 ) = ( vol ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) ) |
| 67 |
|
seq1 |
⊢ ( 1 ∈ ℤ → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ 1 ) ) |
| 68 |
44 67
|
ax-mp |
⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ 1 ) |
| 69 |
|
1nn |
⊢ 1 ∈ ℕ |
| 70 |
|
oveq2 |
⊢ ( 𝑘 = 1 → ( 1 ..^ 𝑘 ) = ( 1 ..^ 1 ) ) |
| 71 |
|
fzo0 |
⊢ ( 1 ..^ 1 ) = ∅ |
| 72 |
70 71
|
eqtrdi |
⊢ ( 𝑘 = 1 → ( 1 ..^ 𝑘 ) = ∅ ) |
| 73 |
72
|
iuneq1d |
⊢ ( 𝑘 = 1 → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) = ∪ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ) |
| 74 |
|
0iun |
⊢ ∪ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) = ∅ |
| 75 |
73 74
|
eqtrdi |
⊢ ( 𝑘 = 1 → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) = ∅ ) |
| 76 |
75
|
difeq2d |
⊢ ( 𝑘 = 1 → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑘 ) ∖ ∅ ) ) |
| 77 |
|
dif0 |
⊢ ( ( 𝐹 ‘ 𝑘 ) ∖ ∅ ) = ( 𝐹 ‘ 𝑘 ) |
| 78 |
76 77
|
eqtrdi |
⊢ ( 𝑘 = 1 → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ( 𝐹 ‘ 𝑘 ) ) |
| 79 |
|
fveq2 |
⊢ ( 𝑘 = 1 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 1 ) ) |
| 80 |
78 79
|
eqtrd |
⊢ ( 𝑘 = 1 → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ( 𝐹 ‘ 1 ) ) |
| 81 |
80
|
fveq2d |
⊢ ( 𝑘 = 1 → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) ) |
| 82 |
|
fvex |
⊢ ( vol ‘ ( 𝐹 ‘ 1 ) ) ∈ V |
| 83 |
81 34 82
|
fvmpt |
⊢ ( 1 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) ) |
| 84 |
69 83
|
ax-mp |
⊢ ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) |
| 85 |
68 84
|
eqtri |
⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) |
| 86 |
85
|
a1i |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 1 ) = ( vol ‘ ( 𝐹 ‘ 1 ) ) ) |
| 87 |
|
oveq1 |
⊢ ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) ) |
| 88 |
|
seqp1 |
⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) ) |
| 89 |
88 6
|
eleq2s |
⊢ ( 𝑗 ∈ ℕ → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) ) |
| 90 |
89
|
adantl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) ) |
| 91 |
|
undif2 |
⊢ ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( ( 𝐹 ‘ 𝑗 ) ∪ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) |
| 92 |
|
fveq2 |
⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ) |
| 93 |
|
fvoveq1 |
⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) |
| 94 |
92 93
|
sseq12d |
⊢ ( 𝑛 = 𝑗 → ( ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐹 ‘ 𝑗 ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) |
| 95 |
|
simpllr |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) |
| 96 |
|
simpr |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ ) |
| 97 |
94 95 96
|
rspcdva |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) |
| 98 |
|
ssequn1 |
⊢ ( ( 𝐹 ‘ 𝑗 ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ↔ ( ( 𝐹 ‘ 𝑗 ) ∪ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) |
| 99 |
97 98
|
sylib |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ∪ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) |
| 100 |
91 99
|
syl5req |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) = ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) |
| 101 |
100
|
fveq2d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( vol ‘ ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) ) |
| 102 |
|
simplll |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝐹 : ℕ ⟶ dom vol ) |
| 103 |
102 96
|
ffvelrnd |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ dom vol ) |
| 104 |
|
peano2nn |
⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ ) |
| 105 |
104
|
adantl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℕ ) |
| 106 |
102 105
|
ffvelrnd |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ dom vol ) |
| 107 |
|
difmbl |
⊢ ( ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ dom vol ∧ ( 𝐹 ‘ 𝑗 ) ∈ dom vol ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ∈ dom vol ) |
| 108 |
106 103 107
|
syl2anc |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ∈ dom vol ) |
| 109 |
|
disjdif |
⊢ ( ( 𝐹 ‘ 𝑗 ) ∩ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ∅ |
| 110 |
109
|
a1i |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ∩ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ∅ ) |
| 111 |
|
2fveq3 |
⊢ ( 𝑘 = 𝑗 → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) |
| 112 |
111
|
eleq1d |
⊢ ( 𝑘 = 𝑗 → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ) ) |
| 113 |
|
simplr |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) |
| 114 |
112 113 96
|
rspcdva |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ) |
| 115 |
|
mblvol |
⊢ ( ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ∈ dom vol → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( vol* ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) |
| 116 |
108 115
|
syl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( vol* ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) |
| 117 |
|
difssd |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) |
| 118 |
|
mblss |
⊢ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ dom vol → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ⊆ ℝ ) |
| 119 |
106 118
|
syl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ⊆ ℝ ) |
| 120 |
|
mblvol |
⊢ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ dom vol → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( vol* ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) |
| 121 |
106 120
|
syl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( vol* ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) |
| 122 |
|
2fveq3 |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) |
| 123 |
122
|
eleq1d |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) ) |
| 124 |
123 113 105
|
rspcdva |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) |
| 125 |
121 124
|
eqeltrrd |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol* ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) |
| 126 |
|
ovolsscl |
⊢ ( ( ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ⊆ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) |
| 127 |
117 119 125 126
|
syl3anc |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol* ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) |
| 128 |
116 127
|
eqeltrd |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) |
| 129 |
|
volun |
⊢ ( ( ( ( 𝐹 ‘ 𝑗 ) ∈ dom vol ∧ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ∈ dom vol ∧ ( ( 𝐹 ‘ 𝑗 ) ∩ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ∅ ) ∧ ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ∧ ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) ) |
| 130 |
103 108 110 114 128 129
|
syl32anc |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ 𝑗 ) ∪ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) ) |
| 131 |
95
|
adantr |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑗 ) ) → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) |
| 132 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... 𝑗 ) → 𝑚 ∈ ℕ ) |
| 133 |
132
|
adantl |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑗 ) ) → 𝑚 ∈ ℕ ) |
| 134 |
|
elfzuz3 |
⊢ ( 𝑚 ∈ ( 1 ... 𝑗 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑚 ) ) |
| 135 |
134
|
adantl |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑗 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑚 ) ) |
| 136 |
|
volsuplem |
⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑚 ) ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) ) |
| 137 |
131 133 135 136
|
syl12anc |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) ) |
| 138 |
137
|
ralrimiva |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) ) |
| 139 |
|
iunss |
⊢ ( ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) ) |
| 140 |
138 139
|
sylibr |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑗 ) ) |
| 141 |
96 6
|
eleqtrdi |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) |
| 142 |
|
eluzfz2 |
⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) → 𝑗 ∈ ( 1 ... 𝑗 ) ) |
| 143 |
141 142
|
syl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( 1 ... 𝑗 ) ) |
| 144 |
|
fveq2 |
⊢ ( 𝑚 = 𝑗 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑗 ) ) |
| 145 |
144
|
ssiun2s |
⊢ ( 𝑗 ∈ ( 1 ... 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ⊆ ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ) |
| 146 |
143 145
|
syl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ⊆ ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) ) |
| 147 |
140 146
|
eqssd |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑗 ) ) |
| 148 |
96
|
nnzd |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ ) |
| 149 |
|
fzval3 |
⊢ ( 𝑗 ∈ ℤ → ( 1 ... 𝑗 ) = ( 1 ..^ ( 𝑗 + 1 ) ) ) |
| 150 |
148 149
|
syl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 1 ... 𝑗 ) = ( 1 ..^ ( 𝑗 + 1 ) ) ) |
| 151 |
150
|
iuneq1d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑚 ) = ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) |
| 152 |
147 151
|
eqtr3d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) |
| 153 |
152
|
difeq2d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) |
| 154 |
153
|
fveq2d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) ) |
| 155 |
|
fveq2 |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) |
| 156 |
|
oveq2 |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 1 ..^ 𝑘 ) = ( 1 ..^ ( 𝑗 + 1 ) ) ) |
| 157 |
156
|
iuneq1d |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) = ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) |
| 158 |
155 157
|
difeq12d |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) |
| 159 |
158
|
fveq2d |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) = ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) ) |
| 160 |
|
fvex |
⊢ ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) ∈ V |
| 161 |
159 34 160
|
fvmpt |
⊢ ( ( 𝑗 + 1 ) ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) ) |
| 162 |
105 161
|
syl |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑚 ∈ ( 1 ..^ ( 𝑗 + 1 ) ) ( 𝐹 ‘ 𝑚 ) ) ) ) |
| 163 |
154 162
|
eqtr4d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) = ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) |
| 164 |
163
|
oveq2d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( vol ‘ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐹 ‘ 𝑗 ) ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) ) |
| 165 |
101 130 164
|
3eqtrd |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) ) |
| 166 |
90 165
|
eqeq12d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ↔ ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) = ( ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) + ( ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ) ) ) |
| 167 |
87 166
|
syl5ibr |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) |
| 168 |
167
|
expcom |
⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) ) |
| 169 |
168
|
a2d |
⊢ ( 𝑗 ∈ ℕ → ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) → ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) ) |
| 170 |
58 62 66 62 86 169
|
nnind |
⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) |
| 171 |
170
|
impcom |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) |
| 172 |
|
fvco3 |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ 𝑗 ∈ ℕ ) → ( ( vol ∘ 𝐹 ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) |
| 173 |
51 172
|
sylan |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( vol ∘ 𝐹 ) ‘ 𝑗 ) = ( vol ‘ ( 𝐹 ‘ 𝑗 ) ) ) |
| 174 |
171 173
|
eqtr4d |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) ‘ 𝑗 ) = ( ( vol ∘ 𝐹 ) ‘ 𝑗 ) ) |
| 175 |
49 54 174
|
eqfnfvd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) = ( vol ∘ 𝐹 ) ) |
| 176 |
175
|
rneqd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) = ran ( vol ∘ 𝐹 ) ) |
| 177 |
|
rnco2 |
⊢ ran ( vol ∘ 𝐹 ) = ( vol “ ran 𝐹 ) |
| 178 |
176 177
|
eqtrdi |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) = ( vol “ ran 𝐹 ) ) |
| 179 |
178
|
supeq1d |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → sup ( ran seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ( 𝐹 ‘ 𝑚 ) ) ) ) ) , ℝ* , < ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) |
| 180 |
36 43 179
|
3eqtr3d |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) |
| 181 |
180
|
ex |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) ) |
| 182 |
|
rexnal |
⊢ ( ∃ 𝑘 ∈ ℕ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ¬ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) |
| 183 |
|
fniunfv |
⊢ ( 𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 ) |
| 184 |
38 183
|
syl |
⊢ ( 𝐹 : ℕ ⟶ dom vol → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 ) |
| 185 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ dom vol ) |
| 186 |
185
|
ralrimiva |
⊢ ( 𝐹 : ℕ ⟶ dom vol → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ dom vol ) |
| 187 |
|
iunmbl |
⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ dom vol → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ dom vol ) |
| 188 |
186 187
|
syl |
⊢ ( 𝐹 : ℕ ⟶ dom vol → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ dom vol ) |
| 189 |
184 188
|
eqeltrrd |
⊢ ( 𝐹 : ℕ ⟶ dom vol → ∪ ran 𝐹 ∈ dom vol ) |
| 190 |
189
|
ad2antrr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ∪ ran 𝐹 ∈ dom vol ) |
| 191 |
|
mblss |
⊢ ( ∪ ran 𝐹 ∈ dom vol → ∪ ran 𝐹 ⊆ ℝ ) |
| 192 |
190 191
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ∪ ran 𝐹 ⊆ ℝ ) |
| 193 |
|
ovolcl |
⊢ ( ∪ ran 𝐹 ⊆ ℝ → ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* ) |
| 194 |
192 193
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* ) |
| 195 |
|
pnfge |
⊢ ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* → ( vol* ‘ ∪ ran 𝐹 ) ≤ +∞ ) |
| 196 |
194 195
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ ran 𝐹 ) ≤ +∞ ) |
| 197 |
|
simprr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) |
| 198 |
1
|
ad2ant2r |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom vol ) |
| 199 |
198 18
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ⊆ ℝ ) |
| 200 |
|
ovolcl |
⊢ ( ( 𝐹 ‘ 𝑘 ) ⊆ ℝ → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* ) |
| 201 |
199 200
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* ) |
| 202 |
|
xrrebnd |
⊢ ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) ) |
| 203 |
201 202
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) ) |
| 204 |
198 20
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
| 205 |
204
|
eleq1d |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) |
| 206 |
|
ovolge0 |
⊢ ( ( 𝐹 ‘ 𝑘 ) ⊆ ℝ → 0 ≤ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
| 207 |
|
mnflt0 |
⊢ -∞ < 0 |
| 208 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
| 209 |
|
0xr |
⊢ 0 ∈ ℝ* |
| 210 |
|
xrltletr |
⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
| 211 |
208 209 210
|
mp3an12 |
⊢ ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* → ( ( -∞ < 0 ∧ 0 ≤ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
| 212 |
207 211
|
mpani |
⊢ ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* → ( 0 ≤ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
| 213 |
200 206 212
|
sylc |
⊢ ( ( 𝐹 ‘ 𝑘 ) ⊆ ℝ → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
| 214 |
199 213
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
| 215 |
214
|
biantrurd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ↔ ( -∞ < ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) ) |
| 216 |
203 205 215
|
3bitr4d |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ↔ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) |
| 217 |
197 216
|
mtbid |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ¬ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) |
| 218 |
|
nltpnft |
⊢ ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ* → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) = +∞ ↔ ¬ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) |
| 219 |
201 218
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) = +∞ ↔ ¬ ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) < +∞ ) ) |
| 220 |
217 219
|
mpbird |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) = +∞ ) |
| 221 |
38
|
ad2antrr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → 𝐹 Fn ℕ ) |
| 222 |
|
simprl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → 𝑘 ∈ ℕ ) |
| 223 |
|
fnfvelrn |
⊢ ( ( 𝐹 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 ) |
| 224 |
221 222 223
|
syl2anc |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 ) |
| 225 |
|
elssuni |
⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 → ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ran 𝐹 ) |
| 226 |
224 225
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ran 𝐹 ) |
| 227 |
|
ovolss |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ ℝ ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) |
| 228 |
226 192 227
|
syl2anc |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( vol* ‘ ∪ ran 𝐹 ) ) |
| 229 |
220 228
|
eqbrtrrd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → +∞ ≤ ( vol* ‘ ∪ ran 𝐹 ) ) |
| 230 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
| 231 |
|
xrletri3 |
⊢ ( ( ( vol* ‘ ∪ ran 𝐹 ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ ↔ ( ( vol* ‘ ∪ ran 𝐹 ) ≤ +∞ ∧ +∞ ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) ) |
| 232 |
194 230 231
|
sylancl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( vol* ‘ ∪ ran 𝐹 ) = +∞ ↔ ( ( vol* ‘ ∪ ran 𝐹 ) ≤ +∞ ∧ +∞ ≤ ( vol* ‘ ∪ ran 𝐹 ) ) ) ) |
| 233 |
196 229 232
|
mpbir2and |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ ran 𝐹 ) = +∞ ) |
| 234 |
|
mblvol |
⊢ ( ∪ ran 𝐹 ∈ dom vol → ( vol ‘ ∪ ran 𝐹 ) = ( vol* ‘ ∪ ran 𝐹 ) ) |
| 235 |
190 234
|
syl |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ∪ ran 𝐹 ) = ( vol* ‘ ∪ ran 𝐹 ) ) |
| 236 |
|
imassrn |
⊢ ( vol “ ran 𝐹 ) ⊆ ran vol |
| 237 |
|
frn |
⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → ran vol ⊆ ( 0 [,] +∞ ) ) |
| 238 |
50 237
|
ax-mp |
⊢ ran vol ⊆ ( 0 [,] +∞ ) |
| 239 |
|
iccssxr |
⊢ ( 0 [,] +∞ ) ⊆ ℝ* |
| 240 |
238 239
|
sstri |
⊢ ran vol ⊆ ℝ* |
| 241 |
236 240
|
sstri |
⊢ ( vol “ ran 𝐹 ) ⊆ ℝ* |
| 242 |
204 220
|
eqtrd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) = +∞ ) |
| 243 |
|
simpll |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → 𝐹 : ℕ ⟶ dom vol ) |
| 244 |
|
ffun |
⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → Fun vol ) |
| 245 |
50 244
|
ax-mp |
⊢ Fun vol |
| 246 |
|
frn |
⊢ ( 𝐹 : ℕ ⟶ dom vol → ran 𝐹 ⊆ dom vol ) |
| 247 |
|
funfvima2 |
⊢ ( ( Fun vol ∧ ran 𝐹 ⊆ dom vol ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( vol “ ran 𝐹 ) ) ) |
| 248 |
245 246 247
|
sylancr |
⊢ ( 𝐹 : ℕ ⟶ dom vol → ( ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( vol “ ran 𝐹 ) ) ) |
| 249 |
243 224 248
|
sylc |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( vol “ ran 𝐹 ) ) |
| 250 |
242 249
|
eqeltrrd |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → +∞ ∈ ( vol “ ran 𝐹 ) ) |
| 251 |
|
supxrpnf |
⊢ ( ( ( vol “ ran 𝐹 ) ⊆ ℝ* ∧ +∞ ∈ ( vol “ ran 𝐹 ) ) → sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) = +∞ ) |
| 252 |
241 250 251
|
sylancr |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) = +∞ ) |
| 253 |
233 235 252
|
3eqtr4d |
⊢ ( ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 𝑘 ∈ ℕ ∧ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) |
| 254 |
253
|
rexlimdvaa |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ∃ 𝑘 ∈ ℕ ¬ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) ) |
| 255 |
182 254
|
syl5bir |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ¬ ∀ 𝑘 ∈ ℕ ( vol ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) ) |
| 256 |
181 255
|
pm2.61d |
⊢ ( ( 𝐹 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( vol ‘ ∪ ran 𝐹 ) = sup ( ( vol “ ran 𝐹 ) , ℝ* , < ) ) |