| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → 𝐴 ∈
dom vol) |
| 2 | 1 | ralimi 3083 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → ∀𝑛
∈ ℕ 𝐴 ∈ dom
vol) |
| 3 | 2 | adantr 480 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ 𝐴 ∈ dom vol) |
| 4 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ 𝐴) = (𝑛 ∈ ℕ ↦ 𝐴) |
| 5 | 4 | fmpt 7130 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
↔ (𝑛 ∈ ℕ
↦ 𝐴):ℕ⟶dom vol) |
| 6 | 3, 5 | sylib 218 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (𝑛 ∈ ℕ ↦ 𝐴):ℕ⟶dom vol) |
| 7 | 4 | fvmpt2 7027 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) → ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = 𝐴) |
| 8 | 7 | adantrr 717 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ)) → ((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛) = 𝐴) |
| 9 | 8 | ralimiaa 3082 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → ∀𝑛
∈ ℕ ((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛) = 𝐴) |
| 10 | | disjeq2 5114 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ ((𝑛 ∈ ℕ
↦ 𝐴)‘𝑛) = 𝐴 → (Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑛 ∈ ℕ 𝐴)) |
| 11 | 9, 10 | syl 17 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → (Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑛 ∈ ℕ 𝐴)) |
| 12 | 11 | biimpar 477 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) |
| 13 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑖((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) |
| 14 | | nffvmpt1 6917 |
. . . . 5
⊢
Ⅎ𝑛((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖) |
| 15 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = 𝑖 → ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) |
| 16 | 13, 14, 15 | cbvdisj 5120 |
. . . 4
⊢
(Disj 𝑛
∈ ℕ ((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑖 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) |
| 17 | 12, 16 | sylib 218 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → Disj 𝑖 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) |
| 18 | | eqid 2737 |
. . 3
⊢ (𝑚 ∈ ℕ ↦
(vol*‘(𝑥 ∩
((𝑛 ∈ ℕ ↦
𝐴)‘𝑚)))) = (𝑚 ∈ ℕ ↦ (vol*‘(𝑥 ∩ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚)))) |
| 19 | | eqid 2737 |
. . 3
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))) |
| 20 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑚(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) |
| 21 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑛vol |
| 22 | | nffvmpt1 6917 |
. . . . 5
⊢
Ⅎ𝑛((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚) |
| 23 | 21, 22 | nffv 6916 |
. . . 4
⊢
Ⅎ𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚)) |
| 24 | | 2fveq3 6911 |
. . . 4
⊢ (𝑛 = 𝑚 → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚))) |
| 25 | 20, 23, 24 | cbvmpt 5253 |
. . 3
⊢ (𝑛 ∈ ℕ ↦
(vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛))) = (𝑚 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚))) |
| 26 | 7 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) →
(vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) |
| 27 | 26 | eleq1d 2826 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) →
((vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ (vol‘𝐴) ∈
ℝ)) |
| 28 | 27 | biimprd 248 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) →
((vol‘𝐴) ∈
ℝ → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ)) |
| 29 | 28 | impr 454 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ)) → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ) |
| 30 | 29 | ralimiaa 3082 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → ∀𝑛
∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ) |
| 31 | 30 | adantr 480 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ) |
| 32 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑖(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ |
| 33 | 21, 14 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) |
| 34 | 33 | nfel1 2922 |
. . . . 5
⊢
Ⅎ𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ |
| 35 | | 2fveq3 6911 |
. . . . . 6
⊢ (𝑛 = 𝑖 → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖))) |
| 36 | 35 | eleq1d 2826 |
. . . . 5
⊢ (𝑛 = 𝑖 → ((vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ)) |
| 37 | 32, 34, 36 | cbvralw 3306 |
. . . 4
⊢
(∀𝑛 ∈
ℕ (vol‘((𝑛
∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ ∀𝑖 ∈ ℕ
(vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ) |
| 38 | 31, 37 | sylib 218 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑖 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ) |
| 39 | 6, 17, 18, 19, 25, 38 | voliunlem3 25587 |
. 2
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ ran (𝑛 ∈ ℕ ↦ 𝐴)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))), ℝ*, <
)) |
| 40 | | dfiun2g 5030 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴}) |
| 41 | 3, 40 | syl 17 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∪
𝑛 ∈ ℕ 𝐴 = ∪
{𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴}) |
| 42 | 4 | rnmpt 5968 |
. . . . 5
⊢ ran
(𝑛 ∈ ℕ ↦
𝐴) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴} |
| 43 | 42 | unieqi 4919 |
. . . 4
⊢ ∪ ran (𝑛 ∈ ℕ ↦ 𝐴) = ∪ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴} |
| 44 | 41, 43 | eqtr4di 2795 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∪
𝑛 ∈ ℕ 𝐴 = ∪
ran (𝑛 ∈ ℕ
↦ 𝐴)) |
| 45 | 44 | fveq2d 6910 |
. 2
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = (vol‘∪
ran (𝑛 ∈ ℕ
↦ 𝐴))) |
| 46 | | voliun.1 |
. . . . 5
⊢ 𝑆 = seq1( + , 𝐺) |
| 47 | | voliun.2 |
. . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘𝐴)) |
| 48 | | eqid 2737 |
. . . . . . . 8
⊢ ℕ =
ℕ |
| 49 | 26 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ)) → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) |
| 50 | 49 | ralimiaa 3082 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → ∀𝑛
∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) |
| 51 | 50 | adantr 480 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) |
| 52 | | mpteq12 5234 |
. . . . . . . 8
⊢ ((ℕ
= ℕ ∧ ∀𝑛
∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) → (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘𝐴))) |
| 53 | 48, 51, 52 | sylancr 587 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘𝐴))) |
| 54 | 47, 53 | eqtr4id 2796 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))) |
| 55 | 54 | seqeq3d 14050 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))))) |
| 56 | 46, 55 | eqtrid 2789 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))))) |
| 57 | 56 | rneqd 5949 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))))) |
| 58 | 57 | supeq1d 9486 |
. 2
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → sup(ran 𝑆, ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑛
∈ ℕ ↦ 𝐴)‘𝑛)))), ℝ*, <
)) |
| 59 | 39, 45, 58 | 3eqtr4d 2787 |
1
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran 𝑆, ℝ*, <
)) |