Step | Hyp | Ref
| Expression |
1 | | catcbas.c |
. . . 4
β’ πΆ = (CatCatβπ) |
2 | | catcbas.u |
. . . 4
β’ (π β π β π) |
3 | | catcbas.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
4 | 1, 3, 2 | catcbas 17992 |
. . . 4
β’ (π β π΅ = (π β© Cat)) |
5 | | eqid 2733 |
. . . . 5
β’ (Hom
βπΆ) = (Hom
βπΆ) |
6 | 1, 3, 2, 5 | catchomfval 17993 |
. . . 4
β’ (π β (Hom βπΆ) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))) |
7 | | eqidd 2734 |
. . . 4
β’ (π β (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π))) = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))) |
8 | 1, 2, 4, 6, 7 | catcval 17991 |
. . 3
β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx),
(Hom βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©}) |
9 | 8 | fveq2d 6847 |
. 2
β’ (π β (compβπΆ) =
(compβ{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (Hom
βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©})) |
10 | | catcco.o |
. 2
β’ Β· =
(compβπΆ) |
11 | 3 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
12 | 11, 11 | xpex 7688 |
. . . 4
β’ (π΅ Γ π΅) β V |
13 | 12, 11 | mpoex 8013 |
. . 3
β’ (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π))) β V |
14 | | catstr 17850 |
. . . 4
β’
{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (Hom
βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©} Struct β¨1, ;15β© |
15 | | ccoid 17300 |
. . . 4
β’ comp =
Slot (compβndx) |
16 | | snsstp3 4779 |
. . . 4
β’
{β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©} β
{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (Hom
βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©} |
17 | 14, 15, 16 | strfv 17081 |
. . 3
β’ ((π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π))) β V β (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π))) =
(compβ{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (Hom
βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©})) |
18 | 13, 17 | ax-mp 5 |
. 2
β’ (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π))) =
(compβ{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (Hom
βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©}) |
19 | 9, 10, 18 | 3eqtr4g 2798 |
1
β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))) |