Step | Hyp | Ref
| Expression |
1 | | chot 29710 |
. 2
class
ยทop |
2 | | vf |
. . 3
setvar ๐ |
3 | | vg |
. . 3
setvar ๐ |
4 | | cc 11007 |
. . 3
class
โ |
5 | | chba 29690 |
. . . 4
class
โ |
6 | | cmap 8723 |
. . . 4
class
โm |
7 | 5, 5, 6 | co 7351 |
. . 3
class ( โ
โm โ) |
8 | | vx |
. . . 4
setvar ๐ฅ |
9 | 2 | cv 1540 |
. . . . 5
class ๐ |
10 | 8 | cv 1540 |
. . . . . 6
class ๐ฅ |
11 | 3 | cv 1540 |
. . . . . 6
class ๐ |
12 | 10, 11 | cfv 6493 |
. . . . 5
class (๐โ๐ฅ) |
13 | | csm 29692 |
. . . . 5
class
ยทโ |
14 | 9, 12, 13 | co 7351 |
. . . 4
class (๐
ยทโ (๐โ๐ฅ)) |
15 | 8, 5, 14 | cmpt 5186 |
. . 3
class (๐ฅ โ โ โฆ (๐
ยทโ (๐โ๐ฅ))) |
16 | 2, 3, 4, 7, 15 | cmpo 7353 |
. 2
class (๐ โ โ, ๐ โ ( โ
โm โ) โฆ (๐ฅ โ โ โฆ (๐ ยทโ (๐โ๐ฅ)))) |
17 | 1, 16 | wceq 1541 |
1
wff
ยทop = (๐ โ โ, ๐ โ ( โ โm โ)
โฆ (๐ฅ โ โ
โฆ (๐
ยทโ (๐โ๐ฅ)))) |