Step | Hyp | Ref
| Expression |
1 | | cfallfac 15892 |
. 2
class
FallFac |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vn |
. . 3
setvar ๐ |
4 | | cc 11054 |
. . 3
class
โ |
5 | | cn0 12418 |
. . 3
class
โ0 |
6 | | cc0 11056 |
. . . . 5
class
0 |
7 | 3 | cv 1541 |
. . . . . 6
class ๐ |
8 | | c1 11057 |
. . . . . 6
class
1 |
9 | | cmin 11390 |
. . . . . 6
class
โ |
10 | 7, 8, 9 | co 7358 |
. . . . 5
class (๐ โ 1) |
11 | | cfz 13430 |
. . . . 5
class
... |
12 | 6, 10, 11 | co 7358 |
. . . 4
class
(0...(๐ โ
1)) |
13 | 2 | cv 1541 |
. . . . 5
class ๐ฅ |
14 | | vk |
. . . . . 6
setvar ๐ |
15 | 14 | cv 1541 |
. . . . 5
class ๐ |
16 | 13, 15, 9 | co 7358 |
. . . 4
class (๐ฅ โ ๐) |
17 | 12, 16, 14 | cprod 15793 |
. . 3
class
โ๐ โ
(0...(๐ โ 1))(๐ฅ โ ๐) |
18 | 2, 3, 4, 5, 17 | cmpo 7360 |
. 2
class (๐ฅ โ โ, ๐ โ โ0
โฆ โ๐ โ
(0...(๐ โ 1))(๐ฅ โ ๐)) |
19 | 1, 18 | wceq 1542 |
1
wff FallFac =
(๐ฅ โ โ, ๐ โ โ0
โฆ โ๐ โ
(0...(๐ โ 1))(๐ฅ โ ๐)) |