Step | Hyp | Ref
| Expression |
1 | | cfuc 17834 |
. 2
class
FuncCat |
2 | | vt |
. . 3
setvar π‘ |
3 | | vu |
. . 3
setvar π’ |
4 | | ccat 17549 |
. . 3
class
Cat |
5 | | cnx 17070 |
. . . . . 6
class
ndx |
6 | | cbs 17088 |
. . . . . 6
class
Base |
7 | 5, 6 | cfv 6497 |
. . . . 5
class
(Baseβndx) |
8 | 2 | cv 1541 |
. . . . . 6
class π‘ |
9 | 3 | cv 1541 |
. . . . . 6
class π’ |
10 | | cfunc 17745 |
. . . . . 6
class
Func |
11 | 8, 9, 10 | co 7358 |
. . . . 5
class (π‘ Func π’) |
12 | 7, 11 | cop 4593 |
. . . 4
class
β¨(Baseβndx), (π‘ Func π’)β© |
13 | | chom 17149 |
. . . . . 6
class
Hom |
14 | 5, 13 | cfv 6497 |
. . . . 5
class (Hom
βndx) |
15 | | cnat 17833 |
. . . . . 6
class
Nat |
16 | 8, 9, 15 | co 7358 |
. . . . 5
class (π‘ Nat π’) |
17 | 14, 16 | cop 4593 |
. . . 4
class
β¨(Hom βndx), (π‘ Nat π’)β© |
18 | | cco 17150 |
. . . . . 6
class
comp |
19 | 5, 18 | cfv 6497 |
. . . . 5
class
(compβndx) |
20 | | vv |
. . . . . 6
setvar π£ |
21 | | vh |
. . . . . 6
setvar β |
22 | 11, 11 | cxp 5632 |
. . . . . 6
class ((π‘ Func π’) Γ (π‘ Func π’)) |
23 | | vf |
. . . . . . 7
setvar π |
24 | 20 | cv 1541 |
. . . . . . . 8
class π£ |
25 | | c1st 7920 |
. . . . . . . 8
class
1st |
26 | 24, 25 | cfv 6497 |
. . . . . . 7
class
(1st βπ£) |
27 | | vg |
. . . . . . . 8
setvar π |
28 | | c2nd 7921 |
. . . . . . . . 9
class
2nd |
29 | 24, 28 | cfv 6497 |
. . . . . . . 8
class
(2nd βπ£) |
30 | | vb |
. . . . . . . . 9
setvar π |
31 | | va |
. . . . . . . . 9
setvar π |
32 | 27 | cv 1541 |
. . . . . . . . . 10
class π |
33 | 21 | cv 1541 |
. . . . . . . . . 10
class β |
34 | 32, 33, 16 | co 7358 |
. . . . . . . . 9
class (π(π‘ Nat π’)β) |
35 | 23 | cv 1541 |
. . . . . . . . . 10
class π |
36 | 35, 32, 16 | co 7358 |
. . . . . . . . 9
class (π(π‘ Nat π’)π) |
37 | | vx |
. . . . . . . . . 10
setvar π₯ |
38 | 8, 6 | cfv 6497 |
. . . . . . . . . 10
class
(Baseβπ‘) |
39 | 37 | cv 1541 |
. . . . . . . . . . . 12
class π₯ |
40 | 30 | cv 1541 |
. . . . . . . . . . . 12
class π |
41 | 39, 40 | cfv 6497 |
. . . . . . . . . . 11
class (πβπ₯) |
42 | 31 | cv 1541 |
. . . . . . . . . . . 12
class π |
43 | 39, 42 | cfv 6497 |
. . . . . . . . . . 11
class (πβπ₯) |
44 | 35, 25 | cfv 6497 |
. . . . . . . . . . . . . 14
class
(1st βπ) |
45 | 39, 44 | cfv 6497 |
. . . . . . . . . . . . 13
class
((1st βπ)βπ₯) |
46 | 32, 25 | cfv 6497 |
. . . . . . . . . . . . . 14
class
(1st βπ) |
47 | 39, 46 | cfv 6497 |
. . . . . . . . . . . . 13
class
((1st βπ)βπ₯) |
48 | 45, 47 | cop 4593 |
. . . . . . . . . . . 12
class
β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© |
49 | 33, 25 | cfv 6497 |
. . . . . . . . . . . . 13
class
(1st ββ) |
50 | 39, 49 | cfv 6497 |
. . . . . . . . . . . 12
class
((1st ββ)βπ₯) |
51 | 9, 18 | cfv 6497 |
. . . . . . . . . . . 12
class
(compβπ’) |
52 | 48, 50, 51 | co 7358 |
. . . . . . . . . . 11
class
(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯)) |
53 | 41, 43, 52 | co 7358 |
. . . . . . . . . 10
class ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)) |
54 | 37, 38, 53 | cmpt 5189 |
. . . . . . . . 9
class (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯))) |
55 | 30, 31, 34, 36, 54 | cmpo 7360 |
. . . . . . . 8
class (π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)))) |
56 | 27, 29, 55 | csb 3856 |
. . . . . . 7
class
β¦(2nd βπ£) / πβ¦(π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)))) |
57 | 23, 26, 56 | csb 3856 |
. . . . . 6
class
β¦(1st βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)))) |
58 | 20, 21, 22, 11, 57 | cmpo 7360 |
. . . . 5
class (π£ β ((π‘ Func π’) Γ (π‘ Func π’)), β β (π‘ Func π’) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯))))) |
59 | 19, 58 | cop 4593 |
. . . 4
class
β¨(compβndx), (π£ β ((π‘ Func π’) Γ (π‘ Func π’)), β β (π‘ Func π’) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)))))β© |
60 | 12, 17, 59 | ctp 4591 |
. . 3
class
{β¨(Baseβndx), (π‘ Func π’)β©, β¨(Hom βndx), (π‘ Nat π’)β©, β¨(compβndx), (π£ β ((π‘ Func π’) Γ (π‘ Func π’)), β β (π‘ Func π’) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)))))β©} |
61 | 2, 3, 4, 4, 60 | cmpo 7360 |
. 2
class (π‘ β Cat, π’ β Cat β¦ {β¨(Baseβndx),
(π‘ Func π’)β©, β¨(Hom βndx), (π‘ Nat π’)β©, β¨(compβndx), (π£ β ((π‘ Func π’) Γ (π‘ Func π’)), β β (π‘ Func π’) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)))))β©}) |
62 | 1, 61 | wceq 1542 |
1
wff FuncCat =
(π‘ β Cat, π’ β Cat β¦
{β¨(Baseβndx), (π‘
Func π’)β©, β¨(Hom
βndx), (π‘ Nat π’)β©, β¨(compβndx),
(π£ β ((π‘ Func π’) Γ (π‘ Func π’)), β β (π‘ Func π’) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)))))β©}) |