Step | Hyp | Ref
| Expression |
1 | | catchomfval.h |
. . 3
β’ π» = (Hom βπΆ) |
2 | | catcbas.c |
. . . . 5
β’ πΆ = (CatCatβπ) |
3 | | catcbas.u |
. . . . 5
β’ (π β π β π) |
4 | | catcbas.b |
. . . . . 6
β’ π΅ = (BaseβπΆ) |
5 | 2, 4, 3 | catcbas 17992 |
. . . . 5
β’ (π β π΅ = (π β© Cat)) |
6 | | eqidd 2734 |
. . . . 5
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦)) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))) |
7 | | eqidd 2734 |
. . . . 5
β’ (π β (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π))) = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))) |
8 | 2, 3, 5, 6, 7 | catcval 17991 |
. . . 4
β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©}) |
9 | 8 | fveq2d 6847 |
. . 3
β’ (π β (Hom βπΆ) = (Hom
β{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©})) |
10 | 1, 9 | eqtrid 2785 |
. 2
β’ (π β π» = (Hom β{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π₯ β
π΅, π¦ β π΅ β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©})) |
11 | 4 | fvexi 6857 |
. . . 4
β’ π΅ β V |
12 | 11, 11 | mpoex 8013 |
. . 3
β’ (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦)) β V |
13 | | catstr 17850 |
. . . 4
β’
{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©} Struct β¨1, ;15β© |
14 | | homid 17298 |
. . . 4
β’ Hom =
Slot (Hom βndx) |
15 | | snsstp2 4778 |
. . . 4
β’
{β¨(Hom βndx), (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))β©} β {β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π₯ β
π΅, π¦ β π΅ β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©} |
16 | 13, 14, 15 | strfv 17081 |
. . 3
β’ ((π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦)) β V β (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦)) = (Hom β{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π₯ β
π΅, π¦ β π΅ β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©})) |
17 | 12, 16 | mp1i 13 |
. 2
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦)) = (Hom β{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π₯ β
π΅, π¦ β π΅ β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©})) |
18 | 10, 17 | eqtr4d 2776 |
1
β’ (π β π» = (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))) |