Step | Hyp | Ref
| Expression |
1 | | funcres.f |
. . . 4
β’ (π β πΉ β (πΆ Func π·)) |
2 | | funcres.h |
. . . 4
β’ (π β π» β (SubcatβπΆ)) |
3 | 1, 2 | resfval 17783 |
. . 3
β’ (π β (πΉ βΎf π») = β¨((1st
βπΉ) βΎ dom dom
π»), (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§)))β©) |
4 | 3 | fveq2d 6847 |
. . . . 5
β’ (π β (2nd
β(πΉ
βΎf π»)) = (2nd
ββ¨((1st βπΉ) βΎ dom dom π»), (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§)))β©)) |
5 | | fvex 6856 |
. . . . . . 7
β’
(1st βπΉ) β V |
6 | 5 | resex 5986 |
. . . . . 6
β’
((1st βπΉ) βΎ dom dom π») β V |
7 | | dmexg 7841 |
. . . . . . 7
β’ (π» β (SubcatβπΆ) β dom π» β V) |
8 | | mptexg 7172 |
. . . . . . 7
β’ (dom
π» β V β (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§))) β V) |
9 | 2, 7, 8 | 3syl 18 |
. . . . . 6
β’ (π β (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§))) β V) |
10 | | op2ndg 7935 |
. . . . . 6
β’
((((1st βπΉ) βΎ dom dom π») β V β§ (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§))) β V) β (2nd
ββ¨((1st βπΉ) βΎ dom dom π»), (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§)))β©) = (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§)))) |
11 | 6, 9, 10 | sylancr 588 |
. . . . 5
β’ (π β (2nd
ββ¨((1st βπΉ) βΎ dom dom π»), (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§)))β©) = (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§)))) |
12 | 4, 11 | eqtrd 2773 |
. . . 4
β’ (π β (2nd
β(πΉ
βΎf π»)) = (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§)))) |
13 | 12 | opeq2d 4838 |
. . 3
β’ (π β β¨((1st
βπΉ) βΎ dom dom
π»), (2nd
β(πΉ
βΎf π»))β© = β¨((1st
βπΉ) βΎ dom dom
π»), (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§)))β©) |
14 | 3, 13 | eqtr4d 2776 |
. 2
β’ (π β (πΉ βΎf π») = β¨((1st
βπΉ) βΎ dom dom
π»), (2nd
β(πΉ
βΎf π»))β©) |
15 | | eqid 2733 |
. . . 4
β’
(Baseβ(πΆ
βΎcat π»)) =
(Baseβ(πΆ
βΎcat π»)) |
16 | | eqid 2733 |
. . . 4
β’
(Baseβπ·) =
(Baseβπ·) |
17 | | eqid 2733 |
. . . 4
β’ (Hom
β(πΆ
βΎcat π»)) =
(Hom β(πΆ
βΎcat π»)) |
18 | | eqid 2733 |
. . . 4
β’ (Hom
βπ·) = (Hom
βπ·) |
19 | | eqid 2733 |
. . . 4
β’
(Idβ(πΆ
βΎcat π»)) =
(Idβ(πΆ
βΎcat π»)) |
20 | | eqid 2733 |
. . . 4
β’
(Idβπ·) =
(Idβπ·) |
21 | | eqid 2733 |
. . . 4
β’
(compβ(πΆ
βΎcat π»)) =
(compβ(πΆ
βΎcat π»)) |
22 | | eqid 2733 |
. . . 4
β’
(compβπ·) =
(compβπ·) |
23 | | eqid 2733 |
. . . . 5
β’ (πΆ βΎcat π») = (πΆ βΎcat π») |
24 | 23, 2 | subccat 17739 |
. . . 4
β’ (π β (πΆ βΎcat π») β Cat) |
25 | | funcrcl 17754 |
. . . . . 6
β’ (πΉ β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
26 | 1, 25 | syl 17 |
. . . . 5
β’ (π β (πΆ β Cat β§ π· β Cat)) |
27 | 26 | simprd 497 |
. . . 4
β’ (π β π· β Cat) |
28 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΆ) =
(BaseβπΆ) |
29 | | relfunc 17753 |
. . . . . . . 8
β’ Rel
(πΆ Func π·) |
30 | | 1st2ndbr 7975 |
. . . . . . . 8
β’ ((Rel
(πΆ Func π·) β§ πΉ β (πΆ Func π·)) β (1st βπΉ)(πΆ Func π·)(2nd βπΉ)) |
31 | 29, 1, 30 | sylancr 588 |
. . . . . . 7
β’ (π β (1st
βπΉ)(πΆ Func π·)(2nd βπΉ)) |
32 | 28, 16, 31 | funcf1 17757 |
. . . . . 6
β’ (π β (1st
βπΉ):(BaseβπΆ)βΆ(Baseβπ·)) |
33 | | eqidd 2734 |
. . . . . . . 8
β’ (π β dom dom π» = dom dom π») |
34 | 2, 33 | subcfn 17732 |
. . . . . . 7
β’ (π β π» Fn (dom dom π» Γ dom dom π»)) |
35 | 2, 34, 28 | subcss1 17733 |
. . . . . 6
β’ (π β dom dom π» β (BaseβπΆ)) |
36 | 32, 35 | fssresd 6710 |
. . . . 5
β’ (π β ((1st
βπΉ) βΎ dom dom
π»):dom dom π»βΆ(Baseβπ·)) |
37 | 26 | simpld 496 |
. . . . . . 7
β’ (π β πΆ β Cat) |
38 | 23, 28, 37, 34, 35 | rescbas 17717 |
. . . . . 6
β’ (π β dom dom π» = (Baseβ(πΆ βΎcat π»))) |
39 | 38 | feq2d 6655 |
. . . . 5
β’ (π β (((1st
βπΉ) βΎ dom dom
π»):dom dom π»βΆ(Baseβπ·) β ((1st
βπΉ) βΎ dom dom
π»):(Baseβ(πΆ βΎcat π»))βΆ(Baseβπ·))) |
40 | 36, 39 | mpbid 231 |
. . . 4
β’ (π β ((1st
βπΉ) βΎ dom dom
π»):(Baseβ(πΆ βΎcat π»))βΆ(Baseβπ·)) |
41 | | fvex 6856 |
. . . . . . 7
β’
((2nd βπΉ)βπ§) β V |
42 | 41 | resex 5986 |
. . . . . 6
β’
(((2nd βπΉ)βπ§) βΎ (π»βπ§)) β V |
43 | | eqid 2733 |
. . . . . 6
β’ (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§))) = (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§))) |
44 | 42, 43 | fnmpti 6645 |
. . . . 5
β’ (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§))) Fn dom π» |
45 | 12 | eqcomd 2739 |
. . . . . 6
β’ (π β (π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§))) = (2nd β(πΉ βΎf
π»))) |
46 | | fndm 6606 |
. . . . . . . 8
β’ (π» Fn (dom dom π» Γ dom dom π») β dom π» = (dom dom π» Γ dom dom π»)) |
47 | 34, 46 | syl 17 |
. . . . . . 7
β’ (π β dom π» = (dom dom π» Γ dom dom π»)) |
48 | 38 | sqxpeqd 5666 |
. . . . . . 7
β’ (π β (dom dom π» Γ dom dom π») = ((Baseβ(πΆ βΎcat π»)) Γ (Baseβ(πΆ βΎcat π»)))) |
49 | 47, 48 | eqtrd 2773 |
. . . . . 6
β’ (π β dom π» = ((Baseβ(πΆ βΎcat π»)) Γ (Baseβ(πΆ βΎcat π»)))) |
50 | 45, 49 | fneq12d 6598 |
. . . . 5
β’ (π β ((π§ β dom π» β¦ (((2nd βπΉ)βπ§) βΎ (π»βπ§))) Fn dom π» β (2nd β(πΉ βΎf
π»)) Fn ((Baseβ(πΆ βΎcat π»)) Γ (Baseβ(πΆ βΎcat π»))))) |
51 | 44, 50 | mpbii 232 |
. . . 4
β’ (π β (2nd
β(πΉ
βΎf π»)) Fn ((Baseβ(πΆ βΎcat π»)) Γ (Baseβ(πΆ βΎcat π»)))) |
52 | | eqid 2733 |
. . . . . . . 8
β’ (Hom
βπΆ) = (Hom
βπΆ) |
53 | 31 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (1st βπΉ)(πΆ Func π·)(2nd βπΉ)) |
54 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β dom dom π» β (BaseβπΆ)) |
55 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π₯ β (Baseβ(πΆ βΎcat π»))) |
56 | 38 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β dom dom π» = (Baseβ(πΆ βΎcat π»))) |
57 | 55, 56 | eleqtrrd 2837 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π₯ β dom dom π») |
58 | 54, 57 | sseldd 3946 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π₯ β (BaseβπΆ)) |
59 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π¦ β (Baseβ(πΆ βΎcat π»))) |
60 | 59, 56 | eleqtrrd 2837 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π¦ β dom dom π») |
61 | 54, 60 | sseldd 3946 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π¦ β (BaseβπΆ)) |
62 | 28, 52, 18, 53, 58, 61 | funcf2 17759 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (π₯(2nd βπΉ)π¦):(π₯(Hom βπΆ)π¦)βΆ(((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΉ)βπ¦))) |
63 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π» β (SubcatβπΆ)) |
64 | 34 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π» Fn (dom dom π» Γ dom dom π»)) |
65 | 63, 64, 52, 57, 60 | subcss2 17734 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (π₯π»π¦) β (π₯(Hom βπΆ)π¦)) |
66 | 62, 65 | fssresd 6710 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β ((π₯(2nd βπΉ)π¦) βΎ (π₯π»π¦)):(π₯π»π¦)βΆ(((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΉ)βπ¦))) |
67 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β πΉ β (πΆ Func π·)) |
68 | 67, 63, 64, 57, 60 | resf2nd 17786 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (π₯(2nd β(πΉ βΎf π»))π¦) = ((π₯(2nd βπΉ)π¦) βΎ (π₯π»π¦))) |
69 | 68 | feq1d 6654 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β ((π₯(2nd β(πΉ βΎf π»))π¦):(π₯π»π¦)βΆ(((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΉ)βπ¦)) β ((π₯(2nd βπΉ)π¦) βΎ (π₯π»π¦)):(π₯π»π¦)βΆ(((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΉ)βπ¦)))) |
70 | 66, 69 | mpbird 257 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (π₯(2nd β(πΉ βΎf π»))π¦):(π₯π»π¦)βΆ(((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΉ)βπ¦))) |
71 | 23, 28, 37, 34, 35 | reschom 17719 |
. . . . . . . 8
β’ (π β π» = (Hom β(πΆ βΎcat π»))) |
72 | 71 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β π» = (Hom β(πΆ βΎcat π»))) |
73 | 72 | oveqd 7375 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (π₯π»π¦) = (π₯(Hom β(πΆ βΎcat π»))π¦)) |
74 | 57 | fvresd 6863 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (((1st βπΉ) βΎ dom dom π»)βπ₯) = ((1st βπΉ)βπ₯)) |
75 | 60 | fvresd 6863 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (((1st βπΉ) βΎ dom dom π»)βπ¦) = ((1st βπΉ)βπ¦)) |
76 | 74, 75 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β ((((1st βπΉ) βΎ dom dom π»)βπ₯)(Hom βπ·)(((1st βπΉ) βΎ dom dom π»)βπ¦)) = (((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΉ)βπ¦))) |
77 | 76 | eqcomd 2739 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΉ)βπ¦)) = ((((1st βπΉ) βΎ dom dom π»)βπ₯)(Hom βπ·)(((1st βπΉ) βΎ dom dom π»)βπ¦))) |
78 | 73, 77 | feq23d 6664 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β ((π₯(2nd β(πΉ βΎf π»))π¦):(π₯π»π¦)βΆ(((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΉ)βπ¦)) β (π₯(2nd β(πΉ βΎf π»))π¦):(π₯(Hom β(πΆ βΎcat π»))π¦)βΆ((((1st βπΉ) βΎ dom dom π»)βπ₯)(Hom βπ·)(((1st βπΉ) βΎ dom dom π»)βπ¦)))) |
79 | 70, 78 | mpbid 231 |
. . . 4
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)))) β (π₯(2nd β(πΉ βΎf π»))π¦):(π₯(Hom β(πΆ βΎcat π»))π¦)βΆ((((1st βπΉ) βΎ dom dom π»)βπ₯)(Hom βπ·)(((1st βπΉ) βΎ dom dom π»)βπ¦))) |
80 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β πΉ β (πΆ Func π·)) |
81 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β π» β (SubcatβπΆ)) |
82 | 34 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β π» Fn (dom dom π» Γ dom dom π»)) |
83 | 38 | eleq2d 2820 |
. . . . . . . 8
β’ (π β (π₯ β dom dom π» β π₯ β (Baseβ(πΆ βΎcat π»)))) |
84 | 83 | biimpar 479 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β π₯ β dom dom π») |
85 | 80, 81, 82, 84, 84 | resf2nd 17786 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β (π₯(2nd β(πΉ βΎf π»))π₯) = ((π₯(2nd βπΉ)π₯) βΎ (π₯π»π₯))) |
86 | | eqid 2733 |
. . . . . . . 8
β’
(IdβπΆ) =
(IdβπΆ) |
87 | 23, 81, 82, 86, 84 | subcid 17738 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β ((IdβπΆ)βπ₯) = ((Idβ(πΆ βΎcat π»))βπ₯)) |
88 | 87 | eqcomd 2739 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β ((Idβ(πΆ βΎcat π»))βπ₯) = ((IdβπΆ)βπ₯)) |
89 | 85, 88 | fveq12d 6850 |
. . . . 5
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β ((π₯(2nd β(πΉ βΎf π»))π₯)β((Idβ(πΆ βΎcat π»))βπ₯)) = (((π₯(2nd βπΉ)π₯) βΎ (π₯π»π₯))β((IdβπΆ)βπ₯))) |
90 | 31 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β (1st βπΉ)(πΆ Func π·)(2nd βπΉ)) |
91 | 38, 35 | eqsstrrd 3984 |
. . . . . . . 8
β’ (π β (Baseβ(πΆ βΎcat π»)) β (BaseβπΆ)) |
92 | 91 | sselda 3945 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β π₯ β (BaseβπΆ)) |
93 | 28, 86, 20, 90, 92 | funcid 17761 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β ((π₯(2nd βπΉ)π₯)β((IdβπΆ)βπ₯)) = ((Idβπ·)β((1st βπΉ)βπ₯))) |
94 | 81, 82, 84, 86 | subcidcl 17735 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) |
95 | 94 | fvresd 6863 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β (((π₯(2nd βπΉ)π₯) βΎ (π₯π»π₯))β((IdβπΆ)βπ₯)) = ((π₯(2nd βπΉ)π₯)β((IdβπΆ)βπ₯))) |
96 | 84 | fvresd 6863 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β (((1st βπΉ) βΎ dom dom π»)βπ₯) = ((1st βπΉ)βπ₯)) |
97 | 96 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β ((Idβπ·)β(((1st βπΉ) βΎ dom dom π»)βπ₯)) = ((Idβπ·)β((1st βπΉ)βπ₯))) |
98 | 93, 95, 97 | 3eqtr4d 2783 |
. . . . 5
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β (((π₯(2nd βπΉ)π₯) βΎ (π₯π»π₯))β((IdβπΆ)βπ₯)) = ((Idβπ·)β(((1st βπΉ) βΎ dom dom π»)βπ₯))) |
99 | 89, 98 | eqtrd 2773 |
. . . 4
β’ ((π β§ π₯ β (Baseβ(πΆ βΎcat π»))) β ((π₯(2nd β(πΉ βΎf π»))π₯)β((Idβ(πΆ βΎcat π»))βπ₯)) = ((Idβπ·)β(((1st βπΉ) βΎ dom dom π»)βπ₯))) |
100 | 2 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π» β (SubcatβπΆ)) |
101 | 34 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π» Fn (dom dom π» Γ dom dom π»)) |
102 | | simp21 1207 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π₯ β (Baseβ(πΆ βΎcat π»))) |
103 | 38 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β dom dom π» = (Baseβ(πΆ βΎcat π»))) |
104 | 102, 103 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π₯ β dom dom π») |
105 | | eqid 2733 |
. . . . . . . 8
β’
(compβπΆ) =
(compβπΆ) |
106 | | simp22 1208 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π¦ β (Baseβ(πΆ βΎcat π»))) |
107 | 106, 103 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π¦ β dom dom π») |
108 | | simp23 1209 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π§ β (Baseβ(πΆ βΎcat π»))) |
109 | 108, 103 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π§ β dom dom π») |
110 | | simp3l 1202 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π β (π₯(Hom β(πΆ βΎcat π»))π¦)) |
111 | 71 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π» = (Hom β(πΆ βΎcat π»))) |
112 | 111 | oveqd 7375 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π₯π»π¦) = (π₯(Hom β(πΆ βΎcat π»))π¦)) |
113 | 110, 112 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π β (π₯π»π¦)) |
114 | | simp3r 1203 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π β (π¦(Hom β(πΆ βΎcat π»))π§)) |
115 | 111 | oveqd 7375 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π¦π»π§) = (π¦(Hom β(πΆ βΎcat π»))π§)) |
116 | 114, 115 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π β (π¦π»π§)) |
117 | 100, 101,
104, 105, 107, 109, 113, 116 | subccocl 17736 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) |
118 | 117 | fvresd 6863 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (((π₯(2nd βπΉ)π§) βΎ (π₯π»π§))β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = ((π₯(2nd βπΉ)π§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π))) |
119 | 31 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (1st βπΉ)(πΆ Func π·)(2nd βπΉ)) |
120 | 35 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β dom dom π» β (BaseβπΆ)) |
121 | 120, 104 | sseldd 3946 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π₯ β (BaseβπΆ)) |
122 | 120, 107 | sseldd 3946 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π¦ β (BaseβπΆ)) |
123 | 120, 109 | sseldd 3946 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π§ β (BaseβπΆ)) |
124 | 100, 101,
52, 104, 107 | subcss2 17734 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π₯π»π¦) β (π₯(Hom βπΆ)π¦)) |
125 | 124, 113 | sseldd 3946 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π β (π₯(Hom βπΆ)π¦)) |
126 | 100, 101,
52, 107, 109 | subcss2 17734 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π¦π»π§) β (π¦(Hom βπΆ)π§)) |
127 | 126, 116 | sseldd 3946 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β π β (π¦(Hom βπΆ)π§)) |
128 | 28, 52, 105, 22, 119, 121, 122, 123, 125, 127 | funcco 17762 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β ((π₯(2nd βπΉ)π§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦(2nd βπΉ)π§)βπ)(β¨((1st βπΉ)βπ₯), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯(2nd βπΉ)π¦)βπ))) |
129 | 118, 128 | eqtrd 2773 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (((π₯(2nd βπΉ)π§) βΎ (π₯π»π§))β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦(2nd βπΉ)π§)βπ)(β¨((1st βπΉ)βπ₯), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯(2nd βπΉ)π¦)βπ))) |
130 | 1 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β πΉ β (πΆ Func π·)) |
131 | 130, 100,
101, 104, 109 | resf2nd 17786 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π₯(2nd β(πΉ βΎf π»))π§) = ((π₯(2nd βπΉ)π§) βΎ (π₯π»π§))) |
132 | 23, 28, 37, 34, 35, 105 | rescco 17721 |
. . . . . . . . . 10
β’ (π β (compβπΆ) = (compβ(πΆ βΎcat π»))) |
133 | 132 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (compβπΆ) = (compβ(πΆ βΎcat π»))) |
134 | 133 | eqcomd 2739 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (compβ(πΆ βΎcat π»)) = (compβπΆ)) |
135 | 134 | oveqd 7375 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (β¨π₯, π¦β©(compβ(πΆ βΎcat π»))π§) = (β¨π₯, π¦β©(compβπΆ)π§)) |
136 | 135 | oveqd 7375 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π(β¨π₯, π¦β©(compβ(πΆ βΎcat π»))π§)π) = (π(β¨π₯, π¦β©(compβπΆ)π§)π)) |
137 | 131, 136 | fveq12d 6850 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β ((π₯(2nd β(πΉ βΎf π»))π§)β(π(β¨π₯, π¦β©(compβ(πΆ βΎcat π»))π§)π)) = (((π₯(2nd βπΉ)π§) βΎ (π₯π»π§))β(π(β¨π₯, π¦β©(compβπΆ)π§)π))) |
138 | 104 | fvresd 6863 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (((1st βπΉ) βΎ dom dom π»)βπ₯) = ((1st βπΉ)βπ₯)) |
139 | 107 | fvresd 6863 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (((1st βπΉ) βΎ dom dom π»)βπ¦) = ((1st βπΉ)βπ¦)) |
140 | 138, 139 | opeq12d 4839 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β β¨(((1st
βπΉ) βΎ dom dom
π»)βπ₯), (((1st βπΉ) βΎ dom dom π»)βπ¦)β© = β¨((1st βπΉ)βπ₯), ((1st βπΉ)βπ¦)β©) |
141 | 109 | fvresd 6863 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (((1st βπΉ) βΎ dom dom π»)βπ§) = ((1st βπΉ)βπ§)) |
142 | 140, 141 | oveq12d 7376 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (β¨(((1st
βπΉ) βΎ dom dom
π»)βπ₯), (((1st βπΉ) βΎ dom dom π»)βπ¦)β©(compβπ·)(((1st βπΉ) βΎ dom dom π»)βπ§)) = (β¨((1st βπΉ)βπ₯), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))) |
143 | 130, 100,
101, 107, 109 | resf2nd 17786 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π¦(2nd β(πΉ βΎf π»))π§) = ((π¦(2nd βπΉ)π§) βΎ (π¦π»π§))) |
144 | 143 | fveq1d 6845 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β ((π¦(2nd β(πΉ βΎf π»))π§)βπ) = (((π¦(2nd βπΉ)π§) βΎ (π¦π»π§))βπ)) |
145 | 116 | fvresd 6863 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (((π¦(2nd βπΉ)π§) βΎ (π¦π»π§))βπ) = ((π¦(2nd βπΉ)π§)βπ)) |
146 | 144, 145 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β ((π¦(2nd β(πΉ βΎf π»))π§)βπ) = ((π¦(2nd βπΉ)π§)βπ)) |
147 | 130, 100,
101, 104, 107 | resf2nd 17786 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (π₯(2nd β(πΉ βΎf π»))π¦) = ((π₯(2nd βπΉ)π¦) βΎ (π₯π»π¦))) |
148 | 147 | fveq1d 6845 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β ((π₯(2nd β(πΉ βΎf π»))π¦)βπ) = (((π₯(2nd βπΉ)π¦) βΎ (π₯π»π¦))βπ)) |
149 | 113 | fvresd 6863 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (((π₯(2nd βπΉ)π¦) βΎ (π₯π»π¦))βπ) = ((π₯(2nd βπΉ)π¦)βπ)) |
150 | 148, 149 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β ((π₯(2nd β(πΉ βΎf π»))π¦)βπ) = ((π₯(2nd βπΉ)π¦)βπ)) |
151 | 142, 146,
150 | oveq123d 7379 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β (((π¦(2nd β(πΉ βΎf π»))π§)βπ)(β¨(((1st βπΉ) βΎ dom dom π»)βπ₯), (((1st βπΉ) βΎ dom dom π»)βπ¦)β©(compβπ·)(((1st βπΉ) βΎ dom dom π»)βπ§))((π₯(2nd β(πΉ βΎf π»))π¦)βπ)) = (((π¦(2nd βπΉ)π§)βπ)(β¨((1st βπΉ)βπ₯), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯(2nd βπΉ)π¦)βπ))) |
152 | 129, 137,
151 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ (π₯ β (Baseβ(πΆ βΎcat π»)) β§ π¦ β (Baseβ(πΆ βΎcat π»)) β§ π§ β (Baseβ(πΆ βΎcat π»))) β§ (π β (π₯(Hom β(πΆ βΎcat π»))π¦) β§ π β (π¦(Hom β(πΆ βΎcat π»))π§))) β ((π₯(2nd β(πΉ βΎf π»))π§)β(π(β¨π₯, π¦β©(compβ(πΆ βΎcat π»))π§)π)) = (((π¦(2nd β(πΉ βΎf π»))π§)βπ)(β¨(((1st βπΉ) βΎ dom dom π»)βπ₯), (((1st βπΉ) βΎ dom dom π»)βπ¦)β©(compβπ·)(((1st βπΉ) βΎ dom dom π»)βπ§))((π₯(2nd β(πΉ βΎf π»))π¦)βπ))) |
153 | 15, 16, 17, 18, 19, 20, 21, 22, 24, 27, 40, 51, 79, 99, 152 | isfuncd 17756 |
. . 3
β’ (π β ((1st
βπΉ) βΎ dom dom
π»)((πΆ βΎcat π») Func π·)(2nd β(πΉ βΎf π»))) |
154 | | df-br 5107 |
. . 3
β’
(((1st βπΉ) βΎ dom dom π»)((πΆ βΎcat π») Func π·)(2nd β(πΉ βΎf π»)) β β¨((1st
βπΉ) βΎ dom dom
π»), (2nd
β(πΉ
βΎf π»))β© β ((πΆ βΎcat π») Func π·)) |
155 | 153, 154 | sylib 217 |
. 2
β’ (π β β¨((1st
βπΉ) βΎ dom dom
π»), (2nd
β(πΉ
βΎf π»))β© β ((πΆ βΎcat π») Func π·)) |
156 | 14, 155 | eqeltrd 2834 |
1
β’ (π β (πΉ βΎf π») β ((πΆ βΎcat π») Func π·)) |