Detailed syntax breakdown of Definition df-exps
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cexps 28405 |
. 2
class
↑s |
| 2 | | vx |
. . 3
setvar 𝑥 |
| 3 | | vy |
. . 3
setvar 𝑦 |
| 4 | | csur 27693 |
. . 3
class No |
| 5 | | czs 28373 |
. . 3
class
ℤs |
| 6 | 3 | cv 1536 |
. . . . 5
class 𝑦 |
| 7 | | c0s 27876 |
. . . . 5
class
0s |
| 8 | 6, 7 | wceq 1537 |
. . . 4
wff 𝑦 =
0s |
| 9 | | c1s 27877 |
. . . 4
class
1s |
| 10 | | cslt 27694 |
. . . . . 6
class
<s |
| 11 | 7, 6, 10 | wbr 5169 |
. . . . 5
wff
0s <s 𝑦 |
| 12 | | cmuls 28141 |
. . . . . . 7
class
·s |
| 13 | | cnns 28328 |
. . . . . . . 8
class
ℕs |
| 14 | 2 | cv 1536 |
. . . . . . . . 9
class 𝑥 |
| 15 | 14 | csn 4648 |
. . . . . . . 8
class {𝑥} |
| 16 | 13, 15 | cxp 5697 |
. . . . . . 7
class
(ℕs × {𝑥}) |
| 17 | 12, 16, 9 | cseqs 28298 |
. . . . . 6
class
seqs 1s ( ·s ,
(ℕs × {𝑥})) |
| 18 | 6, 17 | cfv 6572 |
. . . . 5
class
(seqs 1s ( ·s ,
(ℕs × {𝑥}))‘𝑦) |
| 19 | | cnegs 28060 |
. . . . . . . 8
class
-us |
| 20 | 6, 19 | cfv 6572 |
. . . . . . 7
class (
-us ‘𝑦) |
| 21 | 20, 17 | cfv 6572 |
. . . . . 6
class
(seqs 1s ( ·s ,
(ℕs × {𝑥}))‘( -us ‘𝑦)) |
| 22 | | cdivs 28222 |
. . . . . 6
class
/su |
| 23 | 9, 21, 22 | co 7445 |
. . . . 5
class (
1s /su (seqs 1s (
·s , (ℕs × {𝑥}))‘( -us ‘𝑦))) |
| 24 | 11, 18, 23 | cif 4548 |
. . . 4
class if(
0s <s 𝑦,
(seqs 1s ( ·s , (ℕs
× {𝑥}))‘𝑦), ( 1s
/su (seqs 1s ( ·s ,
(ℕs × {𝑥}))‘( -us ‘𝑦)))) |
| 25 | 8, 9, 24 | cif 4548 |
. . 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 7447 |
. 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 1537 |
1
wff
↑s = (𝑥 ∈ No ,
𝑦 ∈
ℤs ↦ if(𝑦 = 0s , 1s , if(
0s <s 𝑦,
(seqs 1s ( ·s , (ℕs
× {𝑥}))‘𝑦), ( 1s
/su (seqs 1s ( ·s ,
(ℕs × {𝑥}))‘( -us ‘𝑦)))))) |
