Step | Hyp | Ref
| Expression |
1 | | fucbas.q |
. . . . 5
β’ π = (πΆ FuncCat π·) |
2 | | eqid 2732 |
. . . . 5
β’ (πΆ Func π·) = (πΆ Func π·) |
3 | | fuchom.n |
. . . . 5
β’ π = (πΆ Nat π·) |
4 | | eqid 2732 |
. . . . 5
β’
(BaseβπΆ) =
(BaseβπΆ) |
5 | | eqid 2732 |
. . . . 5
β’
(compβπ·) =
(compβπ·) |
6 | | simpl 483 |
. . . . 5
β’ ((πΆ β Cat β§ π· β Cat) β πΆ β Cat) |
7 | | simpr 485 |
. . . . 5
β’ ((πΆ β Cat β§ π· β Cat) β π· β Cat) |
8 | | eqid 2732 |
. . . . . 6
β’
(compβπ) =
(compβπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | fuccofval 17913 |
. . . . 5
β’ ((πΆ β Cat β§ π· β Cat) β
(compβπ) = (π£ β ((πΆ Func π·) Γ (πΆ Func π·)), β β (πΆ Func π·) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β (BaseβπΆ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ·)((1st ββ)βπ₯))(πβπ₯)))))) |
10 | 1, 2, 3, 4, 5, 6, 7, 9 | fucval 17912 |
. . . 4
β’ ((πΆ β Cat β§ π· β Cat) β π = {β¨(Baseβndx),
(πΆ Func π·)β©, β¨(Hom βndx), πβ©, β¨(compβndx),
(compβπ)β©}) |
11 | | catstr 17911 |
. . . 4
β’
{β¨(Baseβndx), (πΆ Func π·)β©, β¨(Hom βndx), πβ©, β¨(compβndx),
(compβπ)β©}
Struct β¨1, ;15β© |
12 | | homid 17359 |
. . . 4
β’ Hom =
Slot (Hom βndx) |
13 | | snsstp2 4820 |
. . . 4
β’
{β¨(Hom βndx), πβ©} β {β¨(Baseβndx),
(πΆ Func π·)β©, β¨(Hom βndx), πβ©, β¨(compβndx),
(compβπ)β©} |
14 | 3 | ovexi 7445 |
. . . . 5
β’ π β V |
15 | 14 | a1i 11 |
. . . 4
β’ ((πΆ β Cat β§ π· β Cat) β π β V) |
16 | | eqid 2732 |
. . . 4
β’ (Hom
βπ) = (Hom
βπ) |
17 | 10, 11, 12, 13, 15, 16 | strfv3 17140 |
. . 3
β’ ((πΆ β Cat β§ π· β Cat) β (Hom
βπ) = π) |
18 | 17 | eqcomd 2738 |
. 2
β’ ((πΆ β Cat β§ π· β Cat) β π = (Hom βπ)) |
19 | | df-hom 17223 |
. . . 4
β’ Hom =
Slot ;14 |
20 | 19 | str0 17124 |
. . 3
β’ β
=
(Hom ββ
) |
21 | 3 | natffn 17902 |
. . . . 5
β’ π Fn ((πΆ Func π·) Γ (πΆ Func π·)) |
22 | | funcrcl 17815 |
. . . . . . . . . 10
β’ (π β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
23 | 22 | con3i 154 |
. . . . . . . . 9
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β Β¬ π β (πΆ Func π·)) |
24 | 23 | eq0rdv 4404 |
. . . . . . . 8
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β (πΆ Func π·) = β
) |
25 | 24 | xpeq2d 5706 |
. . . . . . 7
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β ((πΆ Func π·) Γ (πΆ Func π·)) = ((πΆ Func π·) Γ β
)) |
26 | | xp0 6157 |
. . . . . . 7
β’ ((πΆ Func π·) Γ β
) =
β
|
27 | 25, 26 | eqtrdi 2788 |
. . . . . 6
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β ((πΆ Func π·) Γ (πΆ Func π·)) = β
) |
28 | 27 | fneq2d 6643 |
. . . . 5
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β (π Fn ((πΆ Func π·) Γ (πΆ Func π·)) β π Fn β
)) |
29 | 21, 28 | mpbii 232 |
. . . 4
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β π Fn β
) |
30 | | fn0 6681 |
. . . 4
β’ (π Fn β
β π = β
) |
31 | 29, 30 | sylib 217 |
. . 3
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β π = β
) |
32 | | fnfuc 17898 |
. . . . . . 7
β’ FuncCat
Fn (Cat Γ Cat) |
33 | 32 | fndmi 6653 |
. . . . . 6
β’ dom
FuncCat = (Cat Γ Cat) |
34 | 33 | ndmov 7593 |
. . . . 5
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β (πΆ FuncCat π·) = β
) |
35 | 1, 34 | eqtrid 2784 |
. . . 4
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β π = β
) |
36 | 35 | fveq2d 6895 |
. . 3
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β (Hom
βπ) = (Hom
ββ
)) |
37 | 20, 31, 36 | 3eqtr4a 2798 |
. 2
β’ (Β¬
(πΆ β Cat β§ π· β Cat) β π = (Hom βπ)) |
38 | 18, 37 | pm2.61i 182 |
1
β’ π = (Hom βπ) |