Detailed syntax breakdown of Definition df-sum
| Step | Hyp | Ref
| Expression |
| 1 | | cA |
. . 3
class 𝐴 |
| 2 | | cB |
. . 3
class 𝐵 |
| 3 | | vk |
. . 3
setvar 𝑘 |
| 4 | 1, 2, 3 | csu 15722 |
. 2
class
Σ𝑘 ∈
𝐴 𝐵 |
| 5 | | vm |
. . . . . . . . 9
setvar 𝑚 |
| 6 | 5 | cv 1539 |
. . . . . . . 8
class 𝑚 |
| 7 | | cuz 12878 |
. . . . . . . 8
class
ℤ≥ |
| 8 | 6, 7 | cfv 6561 |
. . . . . . 7
class
(ℤ≥‘𝑚) |
| 9 | 1, 8 | wss 3951 |
. . . . . 6
wff 𝐴 ⊆
(ℤ≥‘𝑚) |
| 10 | | caddc 11158 |
. . . . . . . 8
class
+ |
| 11 | | vn |
. . . . . . . . 9
setvar 𝑛 |
| 12 | | cz 12613 |
. . . . . . . . 9
class
ℤ |
| 13 | 11 | cv 1539 |
. . . . . . . . . . 11
class 𝑛 |
| 14 | 13, 1 | wcel 2108 |
. . . . . . . . . 10
wff 𝑛 ∈ 𝐴 |
| 15 | 3, 13, 2 | csb 3899 |
. . . . . . . . . 10
class
⦋𝑛 /
𝑘⦌𝐵 |
| 16 | | cc0 11155 |
. . . . . . . . . 10
class
0 |
| 17 | 14, 15, 16 | cif 4525 |
. . . . . . . . 9
class if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) |
| 18 | 11, 12, 17 | cmpt 5225 |
. . . . . . . 8
class (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
| 19 | 10, 18, 6 | cseq 14042 |
. . . . . . 7
class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) |
| 20 | | vx |
. . . . . . . 8
setvar 𝑥 |
| 21 | 20 | cv 1539 |
. . . . . . 7
class 𝑥 |
| 22 | | cli 15520 |
. . . . . . 7
class
⇝ |
| 23 | 19, 21, 22 | wbr 5143 |
. . . . . 6
wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 |
| 24 | 9, 23 | wa 395 |
. . . . 5
wff (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) |
| 25 | 24, 5, 12 | wrex 3070 |
. . . 4
wff
∃𝑚 ∈
ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) |
| 26 | | c1 11156 |
. . . . . . . . 9
class
1 |
| 27 | | cfz 13547 |
. . . . . . . . 9
class
... |
| 28 | 26, 6, 27 | co 7431 |
. . . . . . . 8
class
(1...𝑚) |
| 29 | | vf |
. . . . . . . . 9
setvar 𝑓 |
| 30 | 29 | cv 1539 |
. . . . . . . 8
class 𝑓 |
| 31 | 28, 1, 30 | wf1o 6560 |
. . . . . . 7
wff 𝑓:(1...𝑚)–1-1-onto→𝐴 |
| 32 | | cn 12266 |
. . . . . . . . . . 11
class
ℕ |
| 33 | 13, 30 | cfv 6561 |
. . . . . . . . . . . 12
class (𝑓‘𝑛) |
| 34 | 3, 33, 2 | csb 3899 |
. . . . . . . . . . 11
class
⦋(𝑓‘𝑛) / 𝑘⦌𝐵 |
| 35 | 11, 32, 34 | cmpt 5225 |
. . . . . . . . . 10
class (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
| 36 | 10, 35, 26 | cseq 14042 |
. . . . . . . . 9
class seq1( + ,
(𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) |
| 37 | 6, 36 | cfv 6561 |
. . . . . . . 8
class (seq1( +
, (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) |
| 38 | 21, 37 | wceq 1540 |
. . . . . . 7
wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) |
| 39 | 31, 38 | wa 395 |
. . . . . 6
wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
| 40 | 39, 29 | wex 1779 |
. . . . 5
wff
∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
| 41 | 40, 5, 32 | wrex 3070 |
. . . 4
wff
∃𝑚 ∈
ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
| 42 | 25, 41 | wo 848 |
. . 3
wff
(∃𝑚 ∈
ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) |
| 43 | 42, 20 | cio 6512 |
. 2
class
(℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
| 44 | 4, 43 | wceq 1540 |
1
wff
Σ𝑘 ∈
𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |