Step | Hyp | Ref
| Expression |
1 | | cmndtc 47189 |
. 2
class
MndToCat |
2 | | vm |
. . 3
setvar π |
3 | | cmnd 18561 |
. . 3
class
Mnd |
4 | | cnx 17070 |
. . . . . 6
class
ndx |
5 | | cbs 17088 |
. . . . . 6
class
Base |
6 | 4, 5 | cfv 6497 |
. . . . 5
class
(Baseβndx) |
7 | 2 | cv 1541 |
. . . . . 6
class π |
8 | 7 | csn 4587 |
. . . . 5
class {π} |
9 | 6, 8 | cop 4593 |
. . . 4
class
β¨(Baseβndx), {π}β© |
10 | | chom 17149 |
. . . . . 6
class
Hom |
11 | 4, 10 | cfv 6497 |
. . . . 5
class (Hom
βndx) |
12 | 7, 5 | cfv 6497 |
. . . . . . 7
class
(Baseβπ) |
13 | 7, 7, 12 | cotp 4595 |
. . . . . 6
class
β¨π, π, (Baseβπ)β© |
14 | 13 | csn 4587 |
. . . . 5
class
{β¨π, π, (Baseβπ)β©} |
15 | 11, 14 | cop 4593 |
. . . 4
class
β¨(Hom βndx), {β¨π, π, (Baseβπ)β©}β© |
16 | | cco 17150 |
. . . . . 6
class
comp |
17 | 4, 16 | cfv 6497 |
. . . . 5
class
(compβndx) |
18 | 7, 7, 7 | cotp 4595 |
. . . . . . 7
class
β¨π, π, πβ© |
19 | | cplusg 17138 |
. . . . . . . 8
class
+g |
20 | 7, 19 | cfv 6497 |
. . . . . . 7
class
(+gβπ) |
21 | 18, 20 | cop 4593 |
. . . . . 6
class
β¨β¨π, π, πβ©, (+gβπ)β© |
22 | 21 | csn 4587 |
. . . . 5
class
{β¨β¨π,
π, πβ©, (+gβπ)β©} |
23 | 17, 22 | cop 4593 |
. . . 4
class
β¨(compβndx), {β¨β¨π, π, πβ©, (+gβπ)β©}β© |
24 | 9, 15, 23 | ctp 4591 |
. . 3
class
{β¨(Baseβndx), {π}β©, β¨(Hom βndx), {β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©} |
25 | 2, 3, 24 | cmpt 5189 |
. 2
class (π β Mnd β¦
{β¨(Baseβndx), {π}β©, β¨(Hom βndx), {β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©}) |
26 | 1, 25 | wceq 1542 |
1
wff MndToCat =
(π β Mnd β¦
{β¨(Baseβndx), {π}β©, β¨(Hom βndx), {β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©}) |