Step | Hyp | Ref
| Expression |
1 | | cfinsum 36159 |
. 2
class
FinSum |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . . . . . 7
setvar 𝑦 |
4 | 3 | cv 1540 |
. . . . . 6
class 𝑦 |
5 | | ccmn 19647 |
. . . . . 6
class
CMnd |
6 | 4, 5 | wcel 2106 |
. . . . 5
wff 𝑦 ∈ CMnd |
7 | | vt |
. . . . . . . 8
setvar 𝑡 |
8 | 7 | cv 1540 |
. . . . . . 7
class 𝑡 |
9 | | cbs 17143 |
. . . . . . . 8
class
Base |
10 | 4, 9 | cfv 6543 |
. . . . . . 7
class
(Base‘𝑦) |
11 | | vz |
. . . . . . . 8
setvar 𝑧 |
12 | 11 | cv 1540 |
. . . . . . 7
class 𝑧 |
13 | 8, 10, 12 | wf 6539 |
. . . . . 6
wff 𝑧:𝑡⟶(Base‘𝑦) |
14 | | cfn 8938 |
. . . . . 6
class
Fin |
15 | 13, 7, 14 | wrex 3070 |
. . . . 5
wff
∃𝑡 ∈ Fin
𝑧:𝑡⟶(Base‘𝑦) |
16 | 6, 15 | wa 396 |
. . . 4
wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)) |
17 | 16, 3, 11 | copab 5210 |
. . 3
class
{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} |
18 | | c1 11110 |
. . . . . . . . 9
class
1 |
19 | | vm |
. . . . . . . . . 10
setvar 𝑚 |
20 | 19 | cv 1540 |
. . . . . . . . 9
class 𝑚 |
21 | | cfz 13483 |
. . . . . . . . 9
class
... |
22 | 18, 20, 21 | co 7408 |
. . . . . . . 8
class
(1...𝑚) |
23 | 2 | cv 1540 |
. . . . . . . . . 10
class 𝑥 |
24 | | c2nd 7973 |
. . . . . . . . . 10
class
2nd |
25 | 23, 24 | cfv 6543 |
. . . . . . . . 9
class
(2nd ‘𝑥) |
26 | 25 | cdm 5676 |
. . . . . . . 8
class dom
(2nd ‘𝑥) |
27 | | vf |
. . . . . . . . 9
setvar 𝑓 |
28 | 27 | cv 1540 |
. . . . . . . 8
class 𝑓 |
29 | 22, 26, 28 | wf1o 6542 |
. . . . . . 7
wff 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥) |
30 | | vs |
. . . . . . . . 9
setvar 𝑠 |
31 | 30 | cv 1540 |
. . . . . . . 8
class 𝑠 |
32 | | c1st 7972 |
. . . . . . . . . . . 12
class
1st |
33 | 23, 32 | cfv 6543 |
. . . . . . . . . . 11
class
(1st ‘𝑥) |
34 | | cplusg 17196 |
. . . . . . . . . . 11
class
+g |
35 | 33, 34 | cfv 6543 |
. . . . . . . . . 10
class
(+g‘(1st ‘𝑥)) |
36 | | vn |
. . . . . . . . . . 11
setvar 𝑛 |
37 | | cn 12211 |
. . . . . . . . . . 11
class
ℕ |
38 | 36 | cv 1540 |
. . . . . . . . . . . . 13
class 𝑛 |
39 | 38, 28 | cfv 6543 |
. . . . . . . . . . . 12
class (𝑓‘𝑛) |
40 | 39, 25 | cfv 6543 |
. . . . . . . . . . 11
class
((2nd ‘𝑥)‘(𝑓‘𝑛)) |
41 | 36, 37, 40 | cmpt 5231 |
. . . . . . . . . 10
class (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))) |
42 | 35, 41, 18 | cseq 13965 |
. . . . . . . . 9
class
seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛)))) |
43 | 20, 42 | cfv 6543 |
. . . . . . . 8
class
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) |
44 | 31, 43 | wceq 1541 |
. . . . . . 7
wff 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) |
45 | 29, 44 | wa 396 |
. . . . . 6
wff (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) |
46 | 45, 27 | wex 1781 |
. . . . 5
wff
∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) |
47 | | cn0 12471 |
. . . . 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 6493 |
. . 3
class
(℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
50 | 2, 17, 49 | cmpt 5231 |
. 2
class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))) |
51 | 1, 50 | wceq 1541 |
1
wff FinSum =
(𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))) |