Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ π β (πΈ Func π·)) β (Homf
βπΈ) =
(Homf βπΈ)) |
2 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ π β (πΈ Func π·)) β
(compfβπΈ) = (compfβπΈ)) |
3 | | eqid 2733 |
. . . . . . . . 9
β’
(BaseβπΆ) =
(BaseβπΆ) |
4 | | eqid 2733 |
. . . . . . . . 9
β’
(Homf βπΆ) = (Homf βπΆ) |
5 | | resssetc.1 |
. . . . . . . . . . 11
β’ (π β π β π) |
6 | | resssetc.c |
. . . . . . . . . . . 12
β’ πΆ = (SetCatβπ) |
7 | 6 | setccat 17976 |
. . . . . . . . . . 11
β’ (π β π β πΆ β Cat) |
8 | 5, 7 | syl 17 |
. . . . . . . . . 10
β’ (π β πΆ β Cat) |
9 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (πΈ Func π·)) β πΆ β Cat) |
10 | | resssetc.2 |
. . . . . . . . . . 11
β’ (π β π β π) |
11 | 6, 5 | setcbas 17969 |
. . . . . . . . . . 11
β’ (π β π = (BaseβπΆ)) |
12 | 10, 11 | sseqtrd 3985 |
. . . . . . . . . 10
β’ (π β π β (BaseβπΆ)) |
13 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (πΈ Func π·)) β π β (BaseβπΆ)) |
14 | | eqid 2733 |
. . . . . . . . 9
β’ (πΆ βΎs π) = (πΆ βΎs π) |
15 | | eqid 2733 |
. . . . . . . . 9
β’ (πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π))) = (πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π))) |
16 | 3, 4, 9, 13, 14, 15 | fullresc 17742 |
. . . . . . . 8
β’ ((π β§ π β (πΈ Func π·)) β ((Homf
β(πΆ
βΎs π)) =
(Homf β(πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π)))) β§
(compfβ(πΆ βΎs π)) = (compfβ(πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π)))))) |
17 | 16 | simpld 496 |
. . . . . . 7
β’ ((π β§ π β (πΈ Func π·)) β (Homf
β(πΆ
βΎs π)) =
(Homf β(πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π))))) |
18 | | resssetc.d |
. . . . . . . . . 10
β’ π· = (SetCatβπ) |
19 | 6, 18, 5, 10 | resssetc 17983 |
. . . . . . . . 9
β’ (π β ((Homf
β(πΆ
βΎs π)) =
(Homf βπ·) β§
(compfβ(πΆ βΎs π)) = (compfβπ·))) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (πΈ Func π·)) β ((Homf
β(πΆ
βΎs π)) =
(Homf βπ·) β§
(compfβ(πΆ βΎs π)) = (compfβπ·))) |
21 | 20 | simpld 496 |
. . . . . . 7
β’ ((π β§ π β (πΈ Func π·)) β (Homf
β(πΆ
βΎs π)) =
(Homf βπ·)) |
22 | 17, 21 | eqtr3d 2775 |
. . . . . 6
β’ ((π β§ π β (πΈ Func π·)) β (Homf
β(πΆ
βΎcat ((Homf βπΆ) βΎ (π Γ π)))) = (Homf βπ·)) |
23 | 16 | simprd 497 |
. . . . . . 7
β’ ((π β§ π β (πΈ Func π·)) β
(compfβ(πΆ βΎs π)) = (compfβ(πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π))))) |
24 | 20 | simprd 497 |
. . . . . . 7
β’ ((π β§ π β (πΈ Func π·)) β
(compfβ(πΆ βΎs π)) = (compfβπ·)) |
25 | 23, 24 | eqtr3d 2775 |
. . . . . 6
β’ ((π β§ π β (πΈ Func π·)) β
(compfβ(πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π)))) = (compfβπ·)) |
26 | | funcrcl 17754 |
. . . . . . . 8
β’ (π β (πΈ Func π·) β (πΈ β Cat β§ π· β Cat)) |
27 | 26 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (πΈ Func π·)) β (πΈ β Cat β§ π· β Cat)) |
28 | 27 | simpld 496 |
. . . . . 6
β’ ((π β§ π β (πΈ Func π·)) β πΈ β Cat) |
29 | 3, 4, 9, 13 | fullsubc 17741 |
. . . . . . 7
β’ ((π β§ π β (πΈ Func π·)) β ((Homf
βπΆ) βΎ (π Γ π)) β (SubcatβπΆ)) |
30 | 15, 29 | subccat 17739 |
. . . . . 6
β’ ((π β§ π β (πΈ Func π·)) β (πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π))) β Cat) |
31 | 27 | simprd 497 |
. . . . . 6
β’ ((π β§ π β (πΈ Func π·)) β π· β Cat) |
32 | 1, 2, 22, 25, 28, 28, 30, 31 | funcpropd 17792 |
. . . . 5
β’ ((π β§ π β (πΈ Func π·)) β (πΈ Func (πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π)))) = (πΈ Func π·)) |
33 | | funcres2 17789 |
. . . . . 6
β’
(((Homf βπΆ) βΎ (π Γ π)) β (SubcatβπΆ) β (πΈ Func (πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π)))) β (πΈ Func πΆ)) |
34 | 29, 33 | syl 17 |
. . . . 5
β’ ((π β§ π β (πΈ Func π·)) β (πΈ Func (πΆ βΎcat
((Homf βπΆ) βΎ (π Γ π)))) β (πΈ Func πΆ)) |
35 | 32, 34 | eqsstrrd 3984 |
. . . 4
β’ ((π β§ π β (πΈ Func π·)) β (πΈ Func π·) β (πΈ Func πΆ)) |
36 | | simpr 486 |
. . . 4
β’ ((π β§ π β (πΈ Func π·)) β π β (πΈ Func π·)) |
37 | 35, 36 | sseldd 3946 |
. . 3
β’ ((π β§ π β (πΈ Func π·)) β π β (πΈ Func πΆ)) |
38 | 37 | ex 414 |
. 2
β’ (π β (π β (πΈ Func π·) β π β (πΈ Func πΆ))) |
39 | 38 | ssrdv 3951 |
1
β’ (π β (πΈ Func π·) β (πΈ Func πΆ)) |