Detailed syntax breakdown of Definition df-exps
Step | Hyp | Ref
| Expression |
1 | | cexps 28410 |
. 2
class
↑s |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | csur 27698 |
. . 3
class No |
5 | | czs 28378 |
. . 3
class
ℤs |
6 | 3 | cv 1535 |
. . . . 5
class 𝑦 |
7 | | c0s 27881 |
. . . . 5
class
0s |
8 | 6, 7 | wceq 1536 |
. . . 4
wff 𝑦 =
0s |
9 | | c1s 27882 |
. . . 4
class
1s |
10 | | cslt 27699 |
. . . . . 6
class
<s |
11 | 7, 6, 10 | wbr 5147 |
. . . . 5
wff
0s <s 𝑦 |
12 | | cmuls 28146 |
. . . . . . 7
class
·s |
13 | | cnns 28333 |
. . . . . . . 8
class
ℕs |
14 | 2 | cv 1535 |
. . . . . . . . 9
class 𝑥 |
15 | 14 | csn 4630 |
. . . . . . . 8
class {𝑥} |
16 | 13, 15 | cxp 5686 |
. . . . . . 7
class
(ℕs × {𝑥}) |
17 | 12, 16, 9 | cseqs 28303 |
. . . . . 6
class
seqs 1s ( ·s ,
(ℕs × {𝑥})) |
18 | 6, 17 | cfv 6562 |
. . . . 5
class
(seqs 1s ( ·s ,
(ℕs × {𝑥}))‘𝑦) |
19 | | cnegs 28065 |
. . . . . . . 8
class
-us |
20 | 6, 19 | cfv 6562 |
. . . . . . 7
class (
-us ‘𝑦) |
21 | 20, 17 | cfv 6562 |
. . . . . 6
class
(seqs 1s ( ·s ,
(ℕs × {𝑥}))‘( -us ‘𝑦)) |
22 | | cdivs 28227 |
. . . . . 6
class
/su |
23 | 9, 21, 22 | co 7430 |
. . . . 5
class (
1s /su (seqs 1s (
·s , (ℕs × {𝑥}))‘( -us ‘𝑦))) |
24 | 11, 18, 23 | cif 4530 |
. . . 4
class if(
0s <s 𝑦,
(seqs 1s ( ·s , (ℕs
× {𝑥}))‘𝑦), ( 1s
/su (seqs 1s ( ·s ,
(ℕs × {𝑥}))‘( -us ‘𝑦)))) |
25 | 8, 9, 24 | cif 4530 |
. . 3
class if(𝑦 = 0s , 1s
, if( 0s <s 𝑦, (seqs 1s (
·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su
(seqs 1s ( ·s , (ℕs
× {𝑥}))‘(
-us ‘𝑦))))) |
26 | 2, 3, 4, 5, 25 | cmpo 7432 |
. 2
class (𝑥 ∈
No , 𝑦 ∈
ℤs ↦ if(𝑦 = 0s , 1s , if(
0s <s 𝑦,
(seqs 1s ( ·s , (ℕs
× {𝑥}))‘𝑦), ( 1s
/su (seqs 1s ( ·s ,
(ℕs × {𝑥}))‘( -us ‘𝑦)))))) |
27 | 1, 26 | wceq 1536 |
1
wff
↑s = (𝑥 ∈ No ,
𝑦 ∈
ℤs ↦ if(𝑦 = 0s , 1s , if(
0s <s 𝑦,
(seqs 1s ( ·s , (ℕs
× {𝑥}))‘𝑦), ( 1s
/su (seqs 1s ( ·s ,
(ℕs × {𝑥}))‘( -us ‘𝑦)))))) |