Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑘 𝐴 ∈ dom vol |
2 | | nfcsb1v 3515 |
. . . . . 6
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 |
3 | 2 | nfel1 2765 |
. . . . 5
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol |
4 | | csbeq1a 3508 |
. . . . . 6
⊢ (𝑛 = 𝑘 → 𝐴 = ⦋𝑘 / 𝑛⦌𝐴) |
5 | 4 | eleq1d 2672 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝐴 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
6 | 1, 3, 5 | cbvral 3143 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
↔ ∀𝑘 ∈
ℕ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom
vol) |
7 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘𝐴 |
8 | 7, 2, 4 | cbviun 4493 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑘 ∈ ℕ
⦋𝑘 / 𝑛⦌𝐴 |
9 | | csbeq1 3502 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → ⦋𝑘 / 𝑛⦌𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
10 | 9 | iundisj 23123 |
. . . . . 6
⊢ ∪ 𝑘 ∈ ℕ ⦋𝑘 / 𝑛⦌𝐴 = ∪ 𝑘 ∈ ℕ
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) |
11 | 8, 10 | eqtri 2632 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑘 ∈ ℕ
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) |
12 | | difexg 4735 |
. . . . . . 7
⊢
(⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol →
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ V) |
13 | 12 | ralimi 2936 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol →
∀𝑘 ∈ ℕ
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ V) |
14 | | dfiun2g 4488 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ V → ∪ 𝑘 ∈ ℕ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)}) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢
(∀𝑘 ∈
ℕ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol → ∪ 𝑘 ∈ ℕ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)}) |
16 | 11, 15 | syl5eq 2656 |
. . . 4
⊢
(∀𝑘 ∈
ℕ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)}) |
17 | 6, 16 | sylbi 206 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)}) |
18 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ ℕ ↦
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) = (𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) |
19 | 18 | rnmpt 5292 |
. . . 4
⊢ ran
(𝑘 ∈ ℕ ↦
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) = {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)} |
20 | 19 | unieqi 4381 |
. . 3
⊢ ∪ ran (𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) = ∪ {𝑦 ∣ ∃𝑘 ∈ ℕ 𝑦 = (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)} |
21 | 17, 20 | syl6eqr 2662 |
. 2
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ ran (𝑘 ∈ ℕ ↦
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))) |
22 | 3, 5 | rspc 3276 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(∀𝑛 ∈ ℕ
𝐴 ∈ dom vol →
⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
23 | 22 | impcom 445 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom
vol) |
24 | | fzofi 12635 |
. . . . . 6
⊢
(1..^𝑘) ∈
Fin |
25 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑚 𝐴 ∈ dom vol |
26 | | nfcsb1v 3515 |
. . . . . . . . . 10
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
27 | 26 | nfel1 2765 |
. . . . . . . . 9
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol |
28 | | csbeq1a 3508 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
29 | 28 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝐴 ∈ dom vol ↔ ⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol)) |
30 | 25, 27, 29 | cbvral 3143 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
↔ ∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ∈ dom
vol) |
31 | | fzossnn 12384 |
. . . . . . . . 9
⊢
(1..^𝑘) ⊆
ℕ |
32 | | ssralv 3629 |
. . . . . . . . 9
⊢
((1..^𝑘) ⊆
ℕ → (∀𝑚
∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol → ∀𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ∈ dom vol →
∀𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
34 | 30, 33 | sylbi 206 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∀𝑚 ∈
(1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
35 | 34 | adantr 480 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ∀𝑚 ∈
(1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
36 | | finiunmbl 23119 |
. . . . . 6
⊢
(((1..^𝑘) ∈ Fin
∧ ∀𝑚 ∈
(1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) → ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
37 | 24, 35, 36 | sylancr 694 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) |
38 | | difmbl 23118 |
. . . . 5
⊢
((⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol ∧ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 ∈ dom vol) →
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ dom vol) |
39 | 23, 37, 38 | syl2anc 691 |
. . . 4
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) ∈ dom vol) |
40 | 39, 18 | fmptd 6292 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (𝑘 ∈ ℕ
↦ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)):ℕ⟶dom vol) |
41 | | csbeq1 3502 |
. . . . 5
⊢ (𝑖 = 𝑚 → ⦋𝑖 / 𝑛⦌𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
42 | 41 | iundisj2 23124 |
. . . 4
⊢
Disj 𝑖 ∈
ℕ (⦋𝑖 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴) |
43 | | simpr 476 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑖 ∈ ℕ)
→ 𝑖 ∈
ℕ) |
44 | | nfcsb1v 3515 |
. . . . . . . . . 10
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 |
45 | 44 | nfel1 2765 |
. . . . . . . . 9
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ dom vol |
46 | | csbeq1a 3508 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
47 | 46 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑛 = 𝑖 → (𝐴 ∈ dom vol ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ dom vol)) |
48 | 45, 47 | rspc 3276 |
. . . . . . . 8
⊢ (𝑖 ∈ ℕ →
(∀𝑛 ∈ ℕ
𝐴 ∈ dom vol →
⦋𝑖 / 𝑛⦌𝐴 ∈ dom vol)) |
49 | 48 | impcom 445 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑖 ∈ ℕ)
→ ⦋𝑖 /
𝑛⦌𝐴 ∈ dom
vol) |
50 | | difexg 4735 |
. . . . . . 7
⊢
(⦋𝑖 /
𝑛⦌𝐴 ∈ dom vol →
(⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴) ∈ V) |
51 | 49, 50 | syl 17 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑖 ∈ ℕ)
→ (⦋𝑖 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴) ∈ V) |
52 | | csbeq1 3502 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → ⦋𝑘 / 𝑛⦌𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
53 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → (1..^𝑘) = (1..^𝑖)) |
54 | 53 | iuneq1d 4481 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴 = ∪ 𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴) |
55 | 52, 54 | difeq12d 3691 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴) = (⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴)) |
56 | 55, 18 | fvmptg 6189 |
. . . . . 6
⊢ ((𝑖 ∈ ℕ ∧
(⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴) ∈ V) → ((𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑖) = (⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴)) |
57 | 43, 51, 56 | syl2anc 691 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑖 ∈ ℕ)
→ ((𝑘 ∈ ℕ
↦ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑖) = (⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴)) |
58 | 57 | disjeq2dv 4558 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (Disj 𝑖
∈ ℕ ((𝑘 ∈
ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑖) ↔ Disj 𝑖 ∈ ℕ (⦋𝑖 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑖)⦋𝑚 / 𝑛⦌𝐴))) |
59 | 42, 58 | mpbiri 247 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ Disj 𝑖 ∈
ℕ ((𝑘 ∈ ℕ
↦ (⦋𝑘 /
𝑛⦌𝐴 ∖ ∪ 𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑖)) |
60 | | eqid 2610 |
. . 3
⊢ (𝑦 ∈ ℕ ↦
(vol*‘(𝑥 ∩
((𝑘 ∈ ℕ ↦
(⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑦)))) = (𝑦 ∈ ℕ ↦ (vol*‘(𝑥 ∩ ((𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴))‘𝑦)))) |
61 | 40, 59, 60 | voliunlem2 23126 |
. 2
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ ran (𝑘 ∈ ℕ ↦ (⦋𝑘 / 𝑛⦌𝐴 ∖ ∪
𝑚 ∈ (1..^𝑘)⦋𝑚 / 𝑛⦌𝐴)) ∈ dom vol) |
62 | 21, 61 | eqeltrd 2688 |
1
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) |