Step | Hyp | Ref
| Expression |
1 | | cyon 18143 |
. 2
class
Yon |
2 | | vc |
. . 3
setvar ๐ |
3 | | ccat 17549 |
. . 3
class
Cat |
4 | 2 | cv 1541 |
. . . . 5
class ๐ |
5 | | coppc 17596 |
. . . . . 6
class
oppCat |
6 | 4, 5 | cfv 6497 |
. . . . 5
class
(oppCatโ๐) |
7 | 4, 6 | cop 4593 |
. . . 4
class
โจ๐,
(oppCatโ๐)โฉ |
8 | | chof 18142 |
. . . . 5
class
HomF |
9 | 6, 8 | cfv 6497 |
. . . 4
class
(HomFโ(oppCatโ๐)) |
10 | | ccurf 18104 |
. . . 4
class
curryF |
11 | 7, 9, 10 | co 7358 |
. . 3
class
(โจ๐,
(oppCatโ๐)โฉ
curryF (HomFโ(oppCatโ๐))) |
12 | 2, 3, 11 | cmpt 5189 |
. 2
class (๐ โ Cat โฆ (โจ๐, (oppCatโ๐)โฉ curryF
(HomFโ(oppCatโ๐)))) |
13 | 1, 12 | wceq 1542 |
1
wff Yon =
(๐ โ Cat โฆ
(โจ๐,
(oppCatโ๐)โฉ
curryF (HomFโ(oppCatโ๐)))) |