| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑘 𝐴 ∈ dom vol |
| 2 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 |
| 3 | 2 | nfel1 2922 |
. . . . 5
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol |
| 4 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑛 = 𝑘 → 𝐴 = ⦋𝑘 / 𝑛⦌𝐴) |
| 5 | 4 | eleq1d 2826 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝐴 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
| 6 | 1, 3, 5 | cbvralw 3306 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
↔ ∀𝑘 ∈
ℕ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom
vol) |
| 7 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘𝐴 |
| 8 | 7, 2, 4 | cbviun 5036 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑘 ∈ ℕ
⦋𝑘 / 𝑛⦌𝐴 |
| 9 | | csbeq1 3902 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → ⦋𝑘 / 𝑛⦌𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
| 10 | 9 | iundisj 25583 |
. . . . . 6
⊢ ∪ 𝑘 ∈ ℕ ⦋𝑘 / 𝑛⦌𝐴 = ∪ 𝑘 ∈ ℕ
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) |
| 11 | 8, 10 | eqtri 2765 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑘 ∈ ℕ
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) |
| 12 | | difexg 5329 |
. . . . . . 7
⊢
(⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol →
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ V) |
| 13 | 12 | ralimi 3083 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol →
∀𝑘 ∈ ℕ
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ V) |
| 14 | | dfiun2g 5030 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ V → ∪ 𝑘 ∈ ℕ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)}) |
| 15 | 13, 14 | syl 17 |
. . . . 5
⊢
(∀𝑘 ∈
ℕ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol → ∪ 𝑘 ∈ ℕ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)}) |
| 16 | 11, 15 | eqtrid 2789 |
. . . 4
⊢
(∀𝑘 ∈
ℕ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)}) |
| 17 | 6, 16 | sylbi 217 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)}) |
| 18 | | eqid 2737 |
. . . . 5
⊢ (𝑘 ∈ ℕ ↦
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) = (𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) |
| 19 | 18 | rnmpt 5968 |
. . . 4
⊢ ran
(𝑘 ∈ ℕ ↦
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) = {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)} |
| 20 | 19 | unieqi 4919 |
. . 3
⊢ ∪ ran (𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)} |
| 21 | 17, 20 | eqtr4di 2795 |
. 2
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ ran (𝑘 ∈ ℕ ↦
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))) |
| 22 | 3, 5 | rspc 3610 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(∀𝑛 ∈ ℕ
𝐴 ∈ dom vol →
⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
| 23 | 22 | impcom 407 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom
vol) |
| 24 | | fzofi 14015 |
. . . . . 6
⊢
(1..^𝑘) ∈
Fin |
| 25 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑚 𝐴 ∈ dom vol |
| 26 | | nfcsb1v 3923 |
. . . . . . . . . 10
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
| 27 | 26 | nfel1 2922 |
. . . . . . . . 9
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol |
| 28 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
| 29 | 28 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝐴 ∈ dom vol ↔ ⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol)) |
| 30 | 25, 27, 29 | cbvralw 3306 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
↔ ∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ∈ dom
vol) |
| 31 | | fzossnn 13751 |
. . . . . . . . 9
⊢
(1..^𝑘) ⊆
ℕ |
| 32 | | ssralv 4052 |
. . . . . . . . 9
⊢
((1..^𝑘) ⊆
ℕ → (∀𝑚
∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol → ∀𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol)) |
| 33 | 31, 32 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ∈ dom vol →
∀𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
| 34 | 30, 33 | sylbi 217 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∀𝑚 ∈
(1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
| 35 | 34 | adantr 480 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ∀𝑚 ∈
(1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
| 36 | | finiunmbl 25579 |
. . . . . 6
⊢
(((1..^𝑘) ∈ Fin
∧ ∀𝑚 ∈
(1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) → ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
| 37 | 24, 35, 36 | sylancr 587 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
| 38 | | difmbl 25578 |
. . . . 5
⊢
((⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol ∧ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) →
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ dom vol) |
| 39 | 23, 37, 38 | syl2anc 584 |
. . . 4
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ dom vol) |
| 40 | 39 | fmpttd 7135 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (𝑘 ∈ ℕ
↦ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)):ℕ⟶dom vol) |
| 41 | | csbeq1 3902 |
. . . . 5
⊢ (𝑖 = 𝑚 → ⦋𝑖 / 𝑛⦌𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
| 42 | 41 | iundisj2 25584 |
. . . 4
⊢
Disj 𝑖 ∈
ℕ (⦋𝑖 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴) |
| 43 | | csbeq1 3902 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → ⦋𝑘 / 𝑛⦌𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
| 44 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → (1..^𝑘) = (1..^𝑖)) |
| 45 | 44 | iuneq1d 5019 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 = ∪ 𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴) |
| 46 | 43, 45 | difeq12d 4127 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) = (⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴)) |
| 47 | | simpr 484 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑖 ∈ ℕ)
→ 𝑖 ∈
ℕ) |
| 48 | | nfcsb1v 3923 |
. . . . . . . . . 10
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 |
| 49 | 48 | nfel1 2922 |
. . . . . . . . 9
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ dom vol |
| 50 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
| 51 | 50 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑛 = 𝑖 → (𝐴 ∈ dom vol ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ dom vol)) |
| 52 | 49, 51 | rspc 3610 |
. . . . . . . 8
⊢ (𝑖 ∈ ℕ →
(∀𝑛 ∈ ℕ
𝐴 ∈ dom vol →
⦋𝑖 / 𝑛⦌𝐴 ∈ dom vol)) |
| 53 | 52 | impcom 407 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑖 ∈ ℕ)
→ ⦋𝑖 /
𝑛⦌𝐴 ∈ dom
vol) |
| 54 | 53 | difexd 5331 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑖 ∈ ℕ)
→ (⦋𝑖 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴) ∈ V) |
| 55 | 18, 46, 47, 54 | fvmptd3 7039 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑖 ∈ ℕ)
→ ((𝑘 ∈ ℕ
↦ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑖) = (⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴)) |
| 56 | 55 | disjeq2dv 5115 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (Disj 𝑖
∈ ℕ ((𝑘 ∈
ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑖) ↔ Disj 𝑖 ∈ ℕ (⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴))) |
| 57 | 42, 56 | mpbiri 258 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ Disj 𝑖 ∈
ℕ ((𝑘 ∈ ℕ
↦ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑖)) |
| 58 | | eqid 2737 |
. . 3
⊢ (𝑦 ∈ ℕ ↦
(vol*‘(𝑥 ∩
((𝑘 ∈ ℕ ↦
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑦)))) = (𝑦 ∈ ℕ ↦ (vol*‘(𝑥 ∩ ((𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑦)))) |
| 59 | 40, 57, 58 | voliunlem2 25586 |
. 2
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ ran (𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) ∈ dom vol) |
| 60 | 21, 59 | eqeltrd 2841 |
1
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) |