Detailed syntax breakdown of Definition df-sad
Step | Hyp | Ref
| Expression |
1 | | csad 15979 |
. 2
class
sadd |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cn0 12090 |
. . . 4
class
ℕ0 |
5 | 4 | cpw 4513 |
. . 3
class 𝒫
ℕ0 |
6 | | vk |
. . . . . 6
setvar 𝑘 |
7 | 6, 2 | wel 2111 |
. . . . 5
wff 𝑘 ∈ 𝑥 |
8 | 6, 3 | wel 2111 |
. . . . 5
wff 𝑘 ∈ 𝑦 |
9 | | c0 4237 |
. . . . . 6
class
∅ |
10 | 6 | cv 1542 |
. . . . . . 7
class 𝑘 |
11 | | vc |
. . . . . . . . 9
setvar 𝑐 |
12 | | vm |
. . . . . . . . 9
setvar 𝑚 |
13 | | c2o 8196 |
. . . . . . . . 9
class
2o |
14 | 12, 2 | wel 2111 |
. . . . . . . . . . 11
wff 𝑚 ∈ 𝑥 |
15 | 12, 3 | wel 2111 |
. . . . . . . . . . 11
wff 𝑚 ∈ 𝑦 |
16 | 11 | cv 1542 |
. . . . . . . . . . . 12
class 𝑐 |
17 | 9, 16 | wcel 2110 |
. . . . . . . . . . 11
wff ∅
∈ 𝑐 |
18 | 14, 15, 17 | wcad 1613 |
. . . . . . . . . 10
wff cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐) |
19 | | c1o 8195 |
. . . . . . . . . 10
class
1o |
20 | 18, 19, 9 | cif 4439 |
. . . . . . . . 9
class
if(cadd(𝑚 ∈
𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅) |
21 | 11, 12, 13, 4, 20 | cmpo 7215 |
. . . . . . . 8
class (𝑐 ∈ 2o, 𝑚 ∈ ℕ0
↦ if(cadd(𝑚 ∈
𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)) |
22 | | vn |
. . . . . . . . 9
setvar 𝑛 |
23 | 22 | cv 1542 |
. . . . . . . . . . 11
class 𝑛 |
24 | | cc0 10729 |
. . . . . . . . . . 11
class
0 |
25 | 23, 24 | wceq 1543 |
. . . . . . . . . 10
wff 𝑛 = 0 |
26 | | c1 10730 |
. . . . . . . . . . 11
class
1 |
27 | | cmin 11062 |
. . . . . . . . . . 11
class
− |
28 | 23, 26, 27 | co 7213 |
. . . . . . . . . 10
class (𝑛 − 1) |
29 | 25, 9, 28 | cif 4439 |
. . . . . . . . 9
class if(𝑛 = 0, ∅, (𝑛 − 1)) |
30 | 22, 4, 29 | cmpt 5135 |
. . . . . . . 8
class (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))) |
31 | 21, 30, 24 | cseq 13574 |
. . . . . . 7
class
seq0((𝑐 ∈
2o, 𝑚 ∈
ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) |
32 | 10, 31 | cfv 6380 |
. . . . . 6
class
(seq0((𝑐 ∈
2o, 𝑚 ∈
ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑘) |
33 | 9, 32 | wcel 2110 |
. . . . 5
wff ∅
∈ (seq0((𝑐 ∈
2o, 𝑚 ∈
ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑘) |
34 | 7, 8, 33 | whad 1599 |
. . . 4
wff hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑘)) |
35 | 34, 6, 4 | crab 3065 |
. . 3
class {𝑘 ∈ ℕ0
∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑘))} |
36 | 2, 3, 5, 5, 35 | cmpo 7215 |
. 2
class (𝑥 ∈ 𝒫
ℕ0, 𝑦
∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣
hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑘))}) |
37 | 1, 36 | wceq 1543 |
1
wff sadd =
(𝑥 ∈ 𝒫
ℕ0, 𝑦
∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣
hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑘))}) |