Step | Hyp | Ref
| Expression |
1 | | ccatc 17989 |
. 2
class
CatCat |
2 | | vu |
. . 3
setvar π’ |
3 | | cvv 3444 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . 5
class π’ |
6 | | ccat 17549 |
. . . . 5
class
Cat |
7 | 5, 6 | cin 3910 |
. . . 4
class (π’ β© Cat) |
8 | | cnx 17070 |
. . . . . . 7
class
ndx |
9 | | cbs 17088 |
. . . . . . 7
class
Base |
10 | 8, 9 | cfv 6497 |
. . . . . 6
class
(Baseβndx) |
11 | 4 | cv 1541 |
. . . . . 6
class π |
12 | 10, 11 | cop 4593 |
. . . . 5
class
β¨(Baseβndx), πβ© |
13 | | chom 17149 |
. . . . . . 7
class
Hom |
14 | 8, 13 | cfv 6497 |
. . . . . 6
class (Hom
βndx) |
15 | | vx |
. . . . . . 7
setvar π₯ |
16 | | vy |
. . . . . . 7
setvar π¦ |
17 | 15 | cv 1541 |
. . . . . . . 8
class π₯ |
18 | 16 | cv 1541 |
. . . . . . . 8
class π¦ |
19 | | cfunc 17745 |
. . . . . . . 8
class
Func |
20 | 17, 18, 19 | co 7358 |
. . . . . . 7
class (π₯ Func π¦) |
21 | 15, 16, 11, 11, 20 | cmpo 7360 |
. . . . . 6
class (π₯ β π, π¦ β π β¦ (π₯ Func π¦)) |
22 | 14, 21 | cop 4593 |
. . . . 5
class
β¨(Hom βndx), (π₯ β π, π¦ β π β¦ (π₯ Func π¦))β© |
23 | | cco 17150 |
. . . . . . 7
class
comp |
24 | 8, 23 | cfv 6497 |
. . . . . 6
class
(compβndx) |
25 | | vv |
. . . . . . 7
setvar π£ |
26 | | vz |
. . . . . . 7
setvar π§ |
27 | 11, 11 | cxp 5632 |
. . . . . . 7
class (π Γ π) |
28 | | vg |
. . . . . . . 8
setvar π |
29 | | vf |
. . . . . . . 8
setvar π |
30 | 25 | cv 1541 |
. . . . . . . . . 10
class π£ |
31 | | c2nd 7921 |
. . . . . . . . . 10
class
2nd |
32 | 30, 31 | cfv 6497 |
. . . . . . . . 9
class
(2nd βπ£) |
33 | 26 | cv 1541 |
. . . . . . . . 9
class π§ |
34 | 32, 33, 19 | co 7358 |
. . . . . . . 8
class
((2nd βπ£) Func π§) |
35 | 30, 19 | cfv 6497 |
. . . . . . . 8
class ( Func
βπ£) |
36 | 28 | cv 1541 |
. . . . . . . . 9
class π |
37 | 29 | cv 1541 |
. . . . . . . . 9
class π |
38 | | ccofu 17747 |
. . . . . . . . 9
class
βfunc |
39 | 36, 37, 38 | co 7358 |
. . . . . . . 8
class (π βfunc
π) |
40 | 28, 29, 34, 35, 39 | cmpo 7360 |
. . . . . . 7
class (π β ((2nd
βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)) |
41 | 25, 26, 27, 11, 40 | cmpo 7360 |
. . . . . 6
class (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π))) |
42 | 24, 41 | cop 4593 |
. . . . 5
class
β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β© |
43 | 12, 22, 42 | ctp 4591 |
. . . 4
class
{β¨(Baseβndx), πβ©, β¨(Hom βndx), (π₯ β π, π¦ β π β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©} |
44 | 4, 7, 43 | csb 3856 |
. . 3
class
β¦(π’
β© Cat) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
(π₯ β π, π¦ β π β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©} |
45 | 2, 3, 44 | cmpt 5189 |
. 2
class (π’ β V β¦
β¦(π’ β©
Cat) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
(π₯ β π, π¦ β π β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©}) |
46 | 1, 45 | wceq 1542 |
1
wff CatCat =
(π’ β V β¦
β¦(π’ β©
Cat) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
(π₯ β π, π¦ β π β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©}) |