Step | Hyp | Ref
| Expression |
1 | | fucbas.q |
. . . . 5
β’ π = (πΆ FuncCat π·) |
2 | | eqid 2733 |
. . . . 5
β’ (πΆ Func π·) = (πΆ Func π·) |
3 | | fuchom.n |
. . . . 5
β’ π = (πΆ Nat π·) |
4 | | eqid 2733 |
. . . . 5
β’
(BaseβπΆ) =
(BaseβπΆ) |
5 | | eqid 2733 |
. . . . 5
β’
(compβπ·) =
(compβπ·) |
6 | | simpl 484 |
. . . . 5
β’ ((πΆ β Cat β§ π· β Cat) β πΆ β Cat) |
7 | | simpr 486 |
. . . . 5
β’ ((πΆ β Cat β§ π· β Cat) β π· β Cat) |
8 | | eqid 2733 |
. . . . . 6
β’
(compβπ) =
(compβπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | fuccofval 17852 |
. . . . 5
β’ ((πΆ β Cat β§ π· β Cat) β
(compβπ) = (π£ β ((πΆ Func π·) Γ (πΆ Func π·)), β β (πΆ Func π·) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β (BaseβπΆ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ·)((1st ββ)βπ₯))(πβπ₯)))))) |
10 | 1, 2, 3, 4, 5, 6, 7, 9 | fucval 17851 |
. . . 4
β’ ((πΆ β Cat β§ π· β Cat) β π = {β¨(Baseβndx),
(πΆ Func π·)β©, β¨(Hom βndx), πβ©, β¨(compβndx),
(compβπ)β©}) |
11 | | catstr 17850 |
. . . 4
β’
{β¨(Baseβndx), (πΆ Func π·)β©, β¨(Hom βndx), πβ©, β¨(compβndx),
(compβπ)β©}
Struct β¨1, ;15β© |
12 | | homid 17298 |
. . . 4
β’ Hom =
Slot (Hom βndx) |
13 | | snsstp2 4778 |
. . . 4
β’
{β¨(Hom βndx), πβ©} β {β¨(Baseβndx),
(πΆ Func π·)β©, β¨(Hom βndx), πβ©, β¨(compβndx),
(compβπ)β©} |
14 | 3 | ovexi 7392 |
. . . . 5
β’ π β V |
15 | 14 | a1i 11 |
. . . 4
β’ ((πΆ β Cat β§ π· β Cat) β π β V) |
16 | | eqid 2733 |
. . . 4
β’ (Hom
βπ) = (Hom
βπ) |
17 | 10, 11, 12, 13, 15, 16 | strfv3 17082 |
. . 3
β’ ((πΆ β Cat β§ π· β Cat) β (Hom
βπ) = π) |
18 | 17 | eqcomd 2739 |
. 2
β’ ((πΆ β Cat β§ π· β Cat) β π = (Hom βπ)) |
19 | | df-hom 17162 |
. . . 4
β’ Hom =
Slot ;14 |
20 | 19 | str0 17066 |
. . 3
β’ β
=
(Hom ββ
) |
21 | 3 | natffn 17841 |
. . . . 5
β’ π Fn ((πΆ Func π·) Γ (πΆ Func π·)) |
22 | | funcrcl 17754 |
. . . . . . . . . 10
β’ (π β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
23 | 22 | con3i 154 |
. . . . . . . . 9
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β Β¬ π β (πΆ Func π·)) |
24 | 23 | eq0rdv 4365 |
. . . . . . . 8
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β (πΆ Func π·) = β
) |
25 | 24 | xpeq2d 5664 |
. . . . . . 7
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β ((πΆ Func π·) Γ (πΆ Func π·)) = ((πΆ Func π·) Γ β
)) |
26 | | xp0 6111 |
. . . . . . 7
β’ ((πΆ Func π·) Γ β
) =
β
|
27 | 25, 26 | eqtrdi 2789 |
. . . . . 6
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β ((πΆ Func π·) Γ (πΆ Func π·)) = β
) |
28 | 27 | fneq2d 6597 |
. . . . 5
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β (π Fn ((πΆ Func π·) Γ (πΆ Func π·)) β π Fn β
)) |
29 | 21, 28 | mpbii 232 |
. . . 4
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β π Fn β
) |
30 | | fn0 6633 |
. . . 4
β’ (π Fn β
β π = β
) |
31 | 29, 30 | sylib 217 |
. . 3
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β π = β
) |
32 | | fnfuc 17837 |
. . . . . . 7
β’ FuncCat
Fn (Cat Γ Cat) |
33 | 32 | fndmi 6607 |
. . . . . 6
β’ dom
FuncCat = (Cat Γ Cat) |
34 | 33 | ndmov 7539 |
. . . . 5
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β (πΆ FuncCat π·) = β
) |
35 | 1, 34 | eqtrid 2785 |
. . . 4
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β π = β
) |
36 | 35 | fveq2d 6847 |
. . 3
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β (Hom
βπ) = (Hom
ββ
)) |
37 | 20, 31, 36 | 3eqtr4a 2799 |
. 2
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β π = (Hom βπ)) |
38 | 18, 37 | pm2.61i 182 |
1
β’ π = (Hom βπ) |