| 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
|
syl5eq |
⊢ ( ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ 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 |
|
difexg |
⊢ ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ dom vol → ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V ) |
| 55 |
53 54
|
syl |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑖 ∈ ℕ ) → ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V ) |
| 56 |
18 46 47 55
|
fvmptd3 |
⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑖 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑖 ) = ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) |
| 57 |
56
|
disjeq2dv |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ( Disj 𝑖 ∈ ℕ ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑖 ) ↔ Disj 𝑖 ∈ ℕ ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑖 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ) |
| 58 |
42 57
|
mpbiri |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → Disj 𝑖 ∈ ℕ ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑖 ) ) |
| 59 |
|
eqid |
⊢ ( 𝑦 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ ℕ ↦ ( vol* ‘ ( 𝑥 ∩ ( ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ‘ 𝑦 ) ) ) ) |
| 60 |
40 58 59
|
voliunlem2 |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ ran ( 𝑘 ∈ ℕ ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑚 ∈ ( 1 ..^ 𝑘 ) ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ∈ dom vol ) |
| 61 |
21 60
|
eqeltrd |
⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ) |