Step |
Hyp |
Ref |
Expression |
0 |
|
csad |
⊢ sadd |
1 |
|
vx |
⊢ 𝑥 |
2 |
|
cn0 |
⊢ ℕ0 |
3 |
2
|
cpw |
⊢ 𝒫 ℕ0 |
4 |
|
vy |
⊢ 𝑦 |
5 |
|
vk |
⊢ 𝑘 |
6 |
5
|
cv |
⊢ 𝑘 |
7 |
1
|
cv |
⊢ 𝑥 |
8 |
6 7
|
wcel |
⊢ 𝑘 ∈ 𝑥 |
9 |
4
|
cv |
⊢ 𝑦 |
10 |
6 9
|
wcel |
⊢ 𝑘 ∈ 𝑦 |
11 |
|
c0 |
⊢ ∅ |
12 |
|
cc0 |
⊢ 0 |
13 |
|
vc |
⊢ 𝑐 |
14 |
|
c2o |
⊢ 2o |
15 |
|
vm |
⊢ 𝑚 |
16 |
15
|
cv |
⊢ 𝑚 |
17 |
16 7
|
wcel |
⊢ 𝑚 ∈ 𝑥 |
18 |
16 9
|
wcel |
⊢ 𝑚 ∈ 𝑦 |
19 |
13
|
cv |
⊢ 𝑐 |
20 |
11 19
|
wcel |
⊢ ∅ ∈ 𝑐 |
21 |
17 18 20
|
wcad |
⊢ cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) |
22 |
|
c1o |
⊢ 1o |
23 |
21 22 11
|
cif |
⊢ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) |
24 |
13 15 14 2 23
|
cmpo |
⊢ ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) |
25 |
|
vn |
⊢ 𝑛 |
26 |
25
|
cv |
⊢ 𝑛 |
27 |
26 12
|
wceq |
⊢ 𝑛 = 0 |
28 |
|
cmin |
⊢ − |
29 |
|
c1 |
⊢ 1 |
30 |
26 29 28
|
co |
⊢ ( 𝑛 − 1 ) |
31 |
27 11 30
|
cif |
⊢ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) |
32 |
25 2 31
|
cmpt |
⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) |
33 |
24 32 12
|
cseq |
⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) |
34 |
6 33
|
cfv |
⊢ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) |
35 |
11 34
|
wcel |
⊢ ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) |
36 |
8 10 35
|
whad |
⊢ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) |
37 |
36 5 2
|
crab |
⊢ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } |
38 |
1 4 3 3 37
|
cmpo |
⊢ ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } ) |
39 |
0 38
|
wceq |
⊢ sadd = ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } ) |