Step | Hyp | Ref
| Expression |
1 | | chof 18142 |
. 2
class
HomF |
2 | | vc |
. . 3
setvar π |
3 | | ccat 17549 |
. . 3
class
Cat |
4 | 2 | cv 1541 |
. . . . 5
class π |
5 | | chomf 17551 |
. . . . 5
class
Homf |
6 | 4, 5 | cfv 6497 |
. . . 4
class
(Homf βπ) |
7 | | vb |
. . . . 5
setvar π |
8 | | cbs 17088 |
. . . . . 6
class
Base |
9 | 4, 8 | cfv 6497 |
. . . . 5
class
(Baseβπ) |
10 | | vx |
. . . . . 6
setvar π₯ |
11 | | vy |
. . . . . 6
setvar π¦ |
12 | 7 | cv 1541 |
. . . . . . 7
class π |
13 | 12, 12 | cxp 5632 |
. . . . . 6
class (π Γ π) |
14 | | vf |
. . . . . . 7
setvar π |
15 | | vg |
. . . . . . 7
setvar π |
16 | 11 | cv 1541 |
. . . . . . . . 9
class π¦ |
17 | | c1st 7920 |
. . . . . . . . 9
class
1st |
18 | 16, 17 | cfv 6497 |
. . . . . . . 8
class
(1st βπ¦) |
19 | 10 | cv 1541 |
. . . . . . . . 9
class π₯ |
20 | 19, 17 | cfv 6497 |
. . . . . . . 8
class
(1st βπ₯) |
21 | | chom 17149 |
. . . . . . . . 9
class
Hom |
22 | 4, 21 | cfv 6497 |
. . . . . . . 8
class (Hom
βπ) |
23 | 18, 20, 22 | co 7358 |
. . . . . . 7
class
((1st βπ¦)(Hom βπ)(1st βπ₯)) |
24 | | c2nd 7921 |
. . . . . . . . 9
class
2nd |
25 | 19, 24 | cfv 6497 |
. . . . . . . 8
class
(2nd βπ₯) |
26 | 16, 24 | cfv 6497 |
. . . . . . . 8
class
(2nd βπ¦) |
27 | 25, 26, 22 | co 7358 |
. . . . . . 7
class
((2nd βπ₯)(Hom βπ)(2nd βπ¦)) |
28 | | vh |
. . . . . . . 8
setvar β |
29 | 19, 22 | cfv 6497 |
. . . . . . . 8
class ((Hom
βπ)βπ₯) |
30 | 15 | cv 1541 |
. . . . . . . . . 10
class π |
31 | 28 | cv 1541 |
. . . . . . . . . 10
class β |
32 | | cco 17150 |
. . . . . . . . . . . 12
class
comp |
33 | 4, 32 | cfv 6497 |
. . . . . . . . . . 11
class
(compβπ) |
34 | 19, 26, 33 | co 7358 |
. . . . . . . . . 10
class (π₯(compβπ)(2nd βπ¦)) |
35 | 30, 31, 34 | co 7358 |
. . . . . . . . 9
class (π(π₯(compβπ)(2nd βπ¦))β) |
36 | 14 | cv 1541 |
. . . . . . . . 9
class π |
37 | 18, 20 | cop 4593 |
. . . . . . . . . 10
class
β¨(1st βπ¦), (1st βπ₯)β© |
38 | 37, 26, 33 | co 7358 |
. . . . . . . . 9
class
(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦)) |
39 | 35, 36, 38 | co 7358 |
. . . . . . . 8
class ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π) |
40 | 28, 29, 39 | cmpt 5189 |
. . . . . . 7
class (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π)) |
41 | 14, 15, 23, 27, 40 | cmpo 7360 |
. . . . . 6
class (π β ((1st
βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π))) |
42 | 10, 11, 13, 13, 41 | cmpo 7360 |
. . . . 5
class (π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π)))) |
43 | 7, 9, 42 | csb 3856 |
. . . 4
class
β¦(Baseβπ) / πβ¦(π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π)))) |
44 | 6, 43 | cop 4593 |
. . 3
class
β¨(Homf βπ), β¦(Baseβπ) / πβ¦(π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π))))β© |
45 | 2, 3, 44 | cmpt 5189 |
. 2
class (π β Cat β¦
β¨(Homf βπ), β¦(Baseβπ) / πβ¦(π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π))))β©) |
46 | 1, 45 | wceq 1542 |
1
wff
HomF = (π β Cat β¦
β¨(Homf βπ), β¦(Baseβπ) / πβ¦(π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π))))β©) |