Detailed syntax breakdown of Definition df-bj-finsum
| Step | Hyp | Ref
| Expression |
| 1 | | cfinsum 37284 |
. 2
class
FinSum |
| 2 | | vx |
. . 3
setvar 𝑥 |
| 3 | | vy |
. . . . . . 7
setvar 𝑦 |
| 4 | 3 | cv 1539 |
. . . . . 6
class 𝑦 |
| 5 | | ccmn 19798 |
. . . . . 6
class
CMnd |
| 6 | 4, 5 | wcel 2108 |
. . . . 5
wff 𝑦 ∈ CMnd |
| 7 | | vt |
. . . . . . . 8
setvar 𝑡 |
| 8 | 7 | cv 1539 |
. . . . . . 7
class 𝑡 |
| 9 | | cbs 17247 |
. . . . . . . 8
class
Base |
| 10 | 4, 9 | cfv 6561 |
. . . . . . 7
class
(Base‘𝑦) |
| 11 | | vz |
. . . . . . . 8
setvar 𝑧 |
| 12 | 11 | cv 1539 |
. . . . . . 7
class 𝑧 |
| 13 | 8, 10, 12 | wf 6557 |
. . . . . 6
wff 𝑧:𝑡⟶(Base‘𝑦) |
| 14 | | cfn 8985 |
. . . . . 6
class
Fin |
| 15 | 13, 7, 14 | wrex 3070 |
. . . . 5
wff
∃𝑡 ∈ Fin
𝑧:𝑡⟶(Base‘𝑦) |
| 16 | 6, 15 | wa 395 |
. . . 4
wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)) |
| 17 | 16, 3, 11 | copab 5205 |
. . 3
class
{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} |
| 18 | | c1 11156 |
. . . . . . . . 9
class
1 |
| 19 | | vm |
. . . . . . . . . 10
setvar 𝑚 |
| 20 | 19 | cv 1539 |
. . . . . . . . 9
class 𝑚 |
| 21 | | cfz 13547 |
. . . . . . . . 9
class
... |
| 22 | 18, 20, 21 | co 7431 |
. . . . . . . 8
class
(1...𝑚) |
| 23 | 2 | cv 1539 |
. . . . . . . . . 10
class 𝑥 |
| 24 | | c2nd 8013 |
. . . . . . . . . 10
class
2nd |
| 25 | 23, 24 | cfv 6561 |
. . . . . . . . 9
class
(2nd ‘𝑥) |
| 26 | 25 | cdm 5685 |
. . . . . . . 8
class dom
(2nd ‘𝑥) |
| 27 | | vf |
. . . . . . . . 9
setvar 𝑓 |
| 28 | 27 | cv 1539 |
. . . . . . . 8
class 𝑓 |
| 29 | 22, 26, 28 | wf1o 6560 |
. . . . . . 7
wff 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥) |
| 30 | | vs |
. . . . . . . . 9
setvar 𝑠 |
| 31 | 30 | cv 1539 |
. . . . . . . 8
class 𝑠 |
| 32 | | c1st 8012 |
. . . . . . . . . . . 12
class
1st |
| 33 | 23, 32 | cfv 6561 |
. . . . . . . . . . 11
class
(1st ‘𝑥) |
| 34 | | cplusg 17297 |
. . . . . . . . . . 11
class
+g |
| 35 | 33, 34 | cfv 6561 |
. . . . . . . . . 10
class
(+g‘(1st ‘𝑥)) |
| 36 | | vn |
. . . . . . . . . . 11
setvar 𝑛 |
| 37 | | cn 12266 |
. . . . . . . . . . 11
class
ℕ |
| 38 | 36 | cv 1539 |
. . . . . . . . . . . . 13
class 𝑛 |
| 39 | 38, 28 | cfv 6561 |
. . . . . . . . . . . 12
class (𝑓‘𝑛) |
| 40 | 39, 25 | cfv 6561 |
. . . . . . . . . . 11
class
((2nd ‘𝑥)‘(𝑓‘𝑛)) |
| 41 | 36, 37, 40 | cmpt 5225 |
. . . . . . . . . 10
class (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))) |
| 42 | 35, 41, 18 | cseq 14042 |
. . . . . . . . 9
class
seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛)))) |
| 43 | 20, 42 | cfv 6561 |
. . . . . . . 8
class
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) |
| 44 | 31, 43 | wceq 1540 |
. . . . . . 7
wff 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) |
| 45 | 29, 44 | wa 395 |
. . . . . 6
wff (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) |
| 46 | 45, 27 | wex 1779 |
. . . . 5
wff
∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) |
| 47 | | cn0 12526 |
. . . . 5
class
ℕ0 |
| 48 | 46, 19, 47 | wrex 3070 |
. . . 4
wff
∃𝑚 ∈
ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) |
| 49 | 48, 30 | cio 6512 |
. . 3
class
(℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
| 50 | 2, 17, 49 | cmpt 5225 |
. 2
class (𝑥 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))) |
| 51 | 1, 50 | wceq 1540 |
1
wff FinSum =
(𝑥 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))) |