Step |
Hyp |
Ref |
Expression |
1 |
|
nfv |
⊢ Ⅎ 𝑘 𝐴 ∈ dom vol |
2 |
|
nfcsb1v |
⊢ Ⅎ 𝑛 ⦋ 𝑘 / 𝑛 ⦌ 𝐴 |
3 |
2
|
nfel1 |
⊢ Ⅎ 𝑛 ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol |
4 |
|
csbeq1a |
⊢ ( 𝑛 = 𝑘 → 𝐴 = ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) |
5 |
4
|
eleq1d |
⊢ ( 𝑛 = 𝑘 → ( 𝐴 ∈ dom vol ↔ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol ) ) |
6 |
1 3 5
|
cbvralw |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ↔ ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑘 𝐴 |
8 |
7 2 4
|
cbviun |
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 |
9 |
|
csbeq1 |
⊢ ( 𝑘 = 𝑚 → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) |
10 |
9
|
iundisj |
⊢ ∪ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ∪ 𝑘 ∈ ℕ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) |
11 |
8 10
|
eqtri |
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑘 ∈ ℕ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) |
12 |
|
difexg |
⊢ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V ) |
13 |
12
|
ralimi |
⊢ ( ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol → ∀ 𝑘 ∈ ℕ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V ) |
14 |
|
dfiun2g |
⊢ ( ∀ 𝑘 ∈ ℕ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V → ∪ 𝑘 ∈ ℕ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ∪ { 𝑦 ∣ ∃ 𝑘 ∈ ℕ 𝑦 = ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) |
15 |
13 14
|
syl |
⊢ ( ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol → ∪ 𝑘 ∈ ℕ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ∪ { 𝑦 ∣ ∃ 𝑘 ∈ ℕ 𝑦 = ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) |
16 |
11 15
|
eqtrid |
⊢ ( ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 = ∪ { 𝑦 ∣ ∃ 𝑘 ∈ ℕ 𝑦 = ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) |
17 |
6 16
|
sylbi |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 = ∪ { 𝑦 ∣ ∃ 𝑘 ∈ ℕ 𝑦 = ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) |
18 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) = ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) |
19 |
18
|
rnmpt |
⊢ ran ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) = { 𝑦 ∣ ∃ 𝑘 ∈ ℕ 𝑦 = ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } |
20 |
19
|
unieqi |
⊢ ∪ ran ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) = ∪ { 𝑦 ∣ ∃ 𝑘 ∈ ℕ 𝑦 = ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } |
21 |
17 20
|
eqtr4di |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 = ∪ ran ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ) |
22 |
3 5
|
rspc |
⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol ) ) |
23 |
22
|
impcom |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
24 |
|
fzofi |
⊢ ( 1 ..^ 𝑘 ) ∈ Fin |
25 |
|
nfv |
⊢ Ⅎ 𝑚 𝐴 ∈ dom vol |
26 |
|
nfcsb1v |
⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 |
27 |
26
|
nfel1 |
⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol |
28 |
|
csbeq1a |
⊢ ( 𝑛 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) |
29 |
28
|
eleq1d |
⊢ ( 𝑛 = 𝑚 → ( 𝐴 ∈ dom vol ↔ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) ) |
30 |
25 27 29
|
cbvralw |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ↔ ∀ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
31 |
|
fzossnn |
⊢ ( 1 ..^ 𝑘 ) ⊆ ℕ |
32 |
|
ssralv |
⊢ ( ( 1 ..^ 𝑘 ) ⊆ ℕ → ( ∀ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol → ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) ) |
33 |
31 32
|
ax-mp |
⊢ ( ∀ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol → ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
34 |
30 33
|
sylbi |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
35 |
34
|
adantr |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ ) → ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
36 |
|
finiunmbl |
⊢ ( ( ( 1 ..^ 𝑘 ) ∈ Fin ∧ ∀ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
37 |
24 35 36
|
sylancr |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ ) → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
38 |
|
difmbl |
⊢ ( ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol ∧ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ dom vol ) → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ dom vol ) |
39 |
23 37 38
|
syl2anc |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ ) → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ dom vol ) |
40 |
39
|
fmpttd |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) : ℕ ⟶ dom vol ) |
41 |
|
csbeq1 |
⊢ ( 𝑖 = 𝑚 → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) |
42 |
41
|
iundisj2 |
⊢ Disj 𝑖 ∈ ℕ ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) |
43 |
|
csbeq1 |
⊢ ( 𝑘 = 𝑖 → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) |
44 |
|
oveq2 |
⊢ ( 𝑘 = 𝑖 → ( 1 ..^ 𝑘 ) = ( 1 ..^ 𝑖 ) ) |
45 |
44
|
iuneq1d |
⊢ ( 𝑘 = 𝑖 → ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 = ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) |
46 |
43 45
|
difeq12d |
⊢ ( 𝑘 = 𝑖 → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) |
47 |
|
simpr |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ ) |
48 |
|
nfcsb1v |
⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴 |
49 |
48
|
nfel1 |
⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ dom vol |
50 |
|
csbeq1a |
⊢ ( 𝑛 = 𝑖 → 𝐴 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) |
51 |
50
|
eleq1d |
⊢ ( 𝑛 = 𝑖 → ( 𝐴 ∈ dom vol ↔ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ dom vol ) ) |
52 |
49 51
|
rspc |
⊢ ( 𝑖 ∈ ℕ → ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ dom vol ) ) |
53 |
52
|
impcom |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑖 ∈ ℕ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ dom vol ) |
54 |
53
|
difexd |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑖 ∈ ℕ ) → ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V ) |
55 |
18 46 47 54
|
fvmptd3 |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑖 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑖 ) = ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) |
56 |
55
|
disjeq2dv |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ( Disj 𝑖 ∈ ℕ ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑖 ) ↔ Disj 𝑖 ∈ ℕ ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ) |
57 |
42 56
|
mpbiri |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → Disj 𝑖 ∈ ℕ ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑖 ) ) |
58 |
|
eqid |
⊢ ( 𝑦 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑦 ) ) ) ) |
59 |
40 57 58
|
voliunlem2 |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ ran ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ∈ dom vol ) |
60 |
21 59
|
eqeltrd |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ) |