Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → 𝐴 ∈
dom vol) |
2 | 1 | ralimi 3075 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → ∀𝑛
∈ ℕ 𝐴 ∈ dom
vol) |
3 | 2 | adantr 484 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ 𝐴 ∈ dom vol) |
4 | | eqid 2738 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ 𝐴) = (𝑛 ∈ ℕ ↦ 𝐴) |
5 | 4 | fmpt 6885 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
↔ (𝑛 ∈ ℕ
↦ 𝐴):ℕ⟶dom vol) |
6 | 3, 5 | sylib 221 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (𝑛 ∈ ℕ ↦ 𝐴):ℕ⟶dom vol) |
7 | 4 | fvmpt2 6787 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) → ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = 𝐴) |
8 | 7 | adantrr 717 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ)) → ((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛) = 𝐴) |
9 | 8 | ralimiaa 3074 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → ∀𝑛
∈ ℕ ((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛) = 𝐴) |
10 | | disjeq2 5000 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ ((𝑛 ∈ ℕ
↦ 𝐴)‘𝑛) = 𝐴 → (Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑛 ∈ ℕ 𝐴)) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → (Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑛 ∈ ℕ 𝐴)) |
12 | 11 | biimpar 481 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) |
13 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑖((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) |
14 | | nffvmpt1 6686 |
. . . . 5
⊢
Ⅎ𝑛((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖) |
15 | | fveq2 6675 |
. . . . 5
⊢ (𝑛 = 𝑖 → ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) |
16 | 13, 14, 15 | cbvdisj 5006 |
. . . 4
⊢
(Disj 𝑛
∈ ℕ ((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑖 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) |
17 | 12, 16 | sylib 221 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → Disj 𝑖 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) |
18 | | eqid 2738 |
. . 3
⊢ (𝑚 ∈ ℕ ↦
(vol*‘(𝑥 ∩
((𝑛 ∈ ℕ ↦
𝐴)‘𝑚)))) = (𝑚 ∈ ℕ ↦ (vol*‘(𝑥 ∩ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚)))) |
19 | | eqid 2738 |
. . 3
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))) |
20 | | nfcv 2899 |
. . . 4
⊢
Ⅎ𝑚(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) |
21 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑛vol |
22 | | nffvmpt1 6686 |
. . . . 5
⊢
Ⅎ𝑛((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚) |
23 | 21, 22 | nffv 6685 |
. . . 4
⊢
Ⅎ𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚)) |
24 | | 2fveq3 6680 |
. . . 4
⊢ (𝑛 = 𝑚 → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚))) |
25 | 20, 23, 24 | cbvmpt 5132 |
. . 3
⊢ (𝑛 ∈ ℕ ↦
(vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛))) = (𝑚 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚))) |
26 | 7 | fveq2d 6679 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) →
(vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) |
27 | 26 | eleq1d 2817 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) →
((vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ (vol‘𝐴) ∈
ℝ)) |
28 | 27 | biimprd 251 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) →
((vol‘𝐴) ∈
ℝ → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ)) |
29 | 28 | impr 458 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ)) → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ) |
30 | 29 | ralimiaa 3074 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → ∀𝑛
∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ) |
31 | 30 | adantr 484 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ) |
32 | | nfv 1920 |
. . . . 5
⊢
Ⅎ𝑖(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ |
33 | 21, 14 | nffv 6685 |
. . . . . 6
⊢
Ⅎ𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) |
34 | 33 | nfel1 2915 |
. . . . 5
⊢
Ⅎ𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ |
35 | | 2fveq3 6680 |
. . . . . 6
⊢ (𝑛 = 𝑖 → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖))) |
36 | 35 | eleq1d 2817 |
. . . . 5
⊢ (𝑛 = 𝑖 → ((vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ)) |
37 | 32, 34, 36 | cbvralw 3340 |
. . . 4
⊢
(∀𝑛 ∈
ℕ (vol‘((𝑛
∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ ∀𝑖 ∈ ℕ
(vol‘((𝑛 ∈
ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ) |
38 | 31, 37 | sylib 221 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑖 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ) |
39 | 6, 17, 18, 19, 25, 38 | voliunlem3 24305 |
. 2
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ ran (𝑛 ∈ ℕ ↦ 𝐴)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))), ℝ*, <
)) |
40 | | dfiun2g 4918 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴}) |
41 | 3, 40 | syl 17 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∪
𝑛 ∈ ℕ 𝐴 = ∪
{𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴}) |
42 | 4 | rnmpt 5799 |
. . . . 5
⊢ ran
(𝑛 ∈ ℕ ↦
𝐴) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴} |
43 | 42 | unieqi 4810 |
. . . 4
⊢ ∪ ran (𝑛 ∈ ℕ ↦ 𝐴) = ∪ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴} |
44 | 41, 43 | eqtr4di 2791 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∪
𝑛 ∈ ℕ 𝐴 = ∪
ran (𝑛 ∈ ℕ
↦ 𝐴)) |
45 | 44 | fveq2d 6679 |
. 2
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = (vol‘∪
ran (𝑛 ∈ ℕ
↦ 𝐴))) |
46 | | voliun.1 |
. . . . 5
⊢ 𝑆 = seq1( + , 𝐺) |
47 | | voliun.2 |
. . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘𝐴)) |
48 | | eqid 2738 |
. . . . . . . 8
⊢ ℕ =
ℕ |
49 | 26 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ)) → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) |
50 | 49 | ralimiaa 3074 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) → ∀𝑛
∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) |
51 | 50 | adantr 484 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) |
52 | | mpteq12 5118 |
. . . . . . . 8
⊢ ((ℕ
= ℕ ∧ ∀𝑛
∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) → (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘𝐴))) |
53 | 48, 51, 52 | sylancr 590 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘𝐴))) |
54 | 47, 53 | eqtr4id 2792 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))) |
55 | 54 | seqeq3d 13469 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))))) |
56 | 46, 55 | syl5eq 2785 |
. . . 4
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))))) |
57 | 56 | rneqd 5782 |
. . 3
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))))) |
58 | 57 | supeq1d 8984 |
. 2
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → sup(ran 𝑆, ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑛
∈ ℕ ↦ 𝐴)‘𝑛)))), ℝ*, <
)) |
59 | 39, 45, 58 | 3eqtr4d 2783 |
1
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran 𝑆, ℝ*, <
)) |