Step | Hyp | Ref
| Expression |
1 | | df-br 5107 |
. . . . 5
β’ (πΉ(πΆ Func π·)πΊ β β¨πΉ, πΊβ© β (πΆ Func π·)) |
2 | | funcrcl 17754 |
. . . . 5
β’
(β¨πΉ, πΊβ© β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
3 | 1, 2 | sylbi 216 |
. . . 4
β’ (πΉ(πΆ Func π·)πΊ β (πΆ β Cat β§ π· β Cat)) |
4 | 3 | simpld 496 |
. . 3
β’ (πΉ(πΆ Func π·)πΊ β πΆ β Cat) |
5 | 4 | a1i 11 |
. 2
β’ (π β (πΉ(πΆ Func π·)πΊ β πΆ β Cat)) |
6 | | df-br 5107 |
. . . . 5
β’ (πΉ(πΆ Func (π· βΎcat π
))πΊ β β¨πΉ, πΊβ© β (πΆ Func (π· βΎcat π
))) |
7 | | funcrcl 17754 |
. . . . 5
β’
(β¨πΉ, πΊβ© β (πΆ Func (π· βΎcat π
)) β (πΆ β Cat β§ (π· βΎcat π
) β Cat)) |
8 | 6, 7 | sylbi 216 |
. . . 4
β’ (πΉ(πΆ Func (π· βΎcat π
))πΊ β (πΆ β Cat β§ (π· βΎcat π
) β Cat)) |
9 | 8 | simpld 496 |
. . 3
β’ (πΉ(πΆ Func (π· βΎcat π
))πΊ β πΆ β Cat) |
10 | 9 | a1i 11 |
. 2
β’ (π β (πΉ(πΆ Func (π· βΎcat π
))πΊ β πΆ β Cat)) |
11 | | funcres2b.1 |
. . . . . . . 8
β’ (π β πΉ:π΄βΆπ) |
12 | | funcres2b.r |
. . . . . . . . 9
β’ (π β π
β (Subcatβπ·)) |
13 | | funcres2b.s |
. . . . . . . . 9
β’ (π β π
Fn (π Γ π)) |
14 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ·) =
(Baseβπ·) |
15 | 12, 13, 14 | subcss1 17733 |
. . . . . . . 8
β’ (π β π β (Baseβπ·)) |
16 | 11, 15 | fssd 6687 |
. . . . . . 7
β’ (π β πΉ:π΄βΆ(Baseβπ·)) |
17 | | eqid 2733 |
. . . . . . . . . 10
β’ (π· βΎcat π
) = (π· βΎcat π
) |
18 | | subcrcl 17704 |
. . . . . . . . . . 11
β’ (π
β (Subcatβπ·) β π· β Cat) |
19 | 12, 18 | syl 17 |
. . . . . . . . . 10
β’ (π β π· β Cat) |
20 | 17, 14, 19, 13, 15 | rescbas 17717 |
. . . . . . . . 9
β’ (π β π = (Baseβ(π· βΎcat π
))) |
21 | 20 | feq3d 6656 |
. . . . . . . 8
β’ (π β (πΉ:π΄βΆπ β πΉ:π΄βΆ(Baseβ(π· βΎcat π
)))) |
22 | 11, 21 | mpbid 231 |
. . . . . . 7
β’ (π β πΉ:π΄βΆ(Baseβ(π· βΎcat π
))) |
23 | 16, 22 | 2thd 265 |
. . . . . 6
β’ (π β (πΉ:π΄βΆ(Baseβπ·) β πΉ:π΄βΆ(Baseβ(π· βΎcat π
)))) |
24 | 23 | adantr 482 |
. . . . 5
β’ ((π β§ πΆ β Cat) β (πΉ:π΄βΆ(Baseβπ·) β πΉ:π΄βΆ(Baseβ(π· βΎcat π
)))) |
25 | | funcres2b.2 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯πΊπ¦):πβΆ((πΉβπ₯)π
(πΉβπ¦))) |
26 | 25 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯πΊπ¦):πβΆ((πΉβπ₯)π
(πΉβπ¦))) |
27 | 26 | frnd 6677 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β ran (π₯πΊπ¦) β ((πΉβπ₯)π
(πΉβπ¦))) |
28 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β π
β (Subcatβπ·)) |
29 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β π
Fn (π Γ π)) |
30 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (Hom
βπ·) = (Hom
βπ·) |
31 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β πΉ:π΄βΆπ) |
32 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β π₯ β π΄) |
33 | 31, 32 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β (πΉβπ₯) β π) |
34 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β π¦ β π΄) |
35 | 31, 34 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β (πΉβπ¦) β π) |
36 | 28, 29, 30, 33, 35 | subcss2 17734 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((πΉβπ₯)π
(πΉβπ¦)) β ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
37 | 27, 36 | sstrd 3955 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β ran (π₯πΊπ¦) β ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
38 | 37, 27 | 2thd 265 |
. . . . . . . . . . . . 13
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β (ran (π₯πΊπ¦) β ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β ran (π₯πΊπ¦) β ((πΉβπ₯)π
(πΉβπ¦)))) |
39 | 38 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β (((π₯πΊπ¦) Fn (π₯π»π¦) β§ ran (π₯πΊπ¦) β ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) β ((π₯πΊπ¦) Fn (π₯π»π¦) β§ ran (π₯πΊπ¦) β ((πΉβπ₯)π
(πΉβπ¦))))) |
40 | | df-f 6501 |
. . . . . . . . . . . 12
β’ ((π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β ((π₯πΊπ¦) Fn (π₯π»π¦) β§ ran (π₯πΊπ¦) β ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)))) |
41 | | df-f 6501 |
. . . . . . . . . . . 12
β’ ((π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)π
(πΉβπ¦)) β ((π₯πΊπ¦) Fn (π₯π»π¦) β§ ran (π₯πΊπ¦) β ((πΉβπ₯)π
(πΉβπ¦)))) |
42 | 39, 40, 41 | 3bitr4g 314 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)π
(πΉβπ¦)))) |
43 | 17, 14, 19, 13, 15 | reschom 17719 |
. . . . . . . . . . . . . 14
β’ (π β π
= (Hom β(π· βΎcat π
))) |
44 | 43 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β π
= (Hom β(π· βΎcat π
))) |
45 | 44 | oveqd 7375 |
. . . . . . . . . . . 12
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((πΉβπ₯)π
(πΉβπ¦)) = ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦))) |
46 | 45 | feq3d 6656 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)π
(πΉβπ¦)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)))) |
47 | 42, 46 | bitrd 279 |
. . . . . . . . . 10
β’ (((π β§ πΆ β Cat) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)))) |
48 | 47 | ralrimivva 3194 |
. . . . . . . . 9
β’ ((π β§ πΆ β Cat) β βπ₯ β π΄ βπ¦ β π΄ ((π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)))) |
49 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π§ = β¨π₯, π¦β© β (πΊβπ§) = (πΊββ¨π₯, π¦β©)) |
50 | | df-ov 7361 |
. . . . . . . . . . . . . 14
β’ (π₯πΊπ¦) = (πΊββ¨π₯, π¦β©) |
51 | 49, 50 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ (π§ = β¨π₯, π¦β© β (πΊβπ§) = (π₯πΊπ¦)) |
52 | | vex 3448 |
. . . . . . . . . . . . . . . . 17
β’ π₯ β V |
53 | | vex 3448 |
. . . . . . . . . . . . . . . . 17
β’ π¦ β V |
54 | 52, 53 | op1std 7932 |
. . . . . . . . . . . . . . . 16
β’ (π§ = β¨π₯, π¦β© β (1st βπ§) = π₯) |
55 | 54 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (π§ = β¨π₯, π¦β© β (πΉβ(1st βπ§)) = (πΉβπ₯)) |
56 | 52, 53 | op2ndd 7933 |
. . . . . . . . . . . . . . . 16
β’ (π§ = β¨π₯, π¦β© β (2nd βπ§) = π¦) |
57 | 56 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (π§ = β¨π₯, π¦β© β (πΉβ(2nd βπ§)) = (πΉβπ¦)) |
58 | 55, 57 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (π§ = β¨π₯, π¦β© β ((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) = ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
59 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’ (π§ = β¨π₯, π¦β© β (π»βπ§) = (π»ββ¨π₯, π¦β©)) |
60 | | df-ov 7361 |
. . . . . . . . . . . . . . 15
β’ (π₯π»π¦) = (π»ββ¨π₯, π¦β©) |
61 | 59, 60 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ (π§ = β¨π₯, π¦β© β (π»βπ§) = (π₯π»π¦)) |
62 | 58, 61 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π§ = β¨π₯, π¦β© β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) = (((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) βm (π₯π»π¦))) |
63 | 51, 62 | eleq12d 2828 |
. . . . . . . . . . . 12
β’ (π§ = β¨π₯, π¦β© β ((πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β (π₯πΊπ¦) β (((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) βm (π₯π»π¦)))) |
64 | | ovex 7391 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β V |
65 | | ovex 7391 |
. . . . . . . . . . . . 13
β’ (π₯π»π¦) β V |
66 | 64, 65 | elmap 8812 |
. . . . . . . . . . . 12
β’ ((π₯πΊπ¦) β (((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) βm (π₯π»π¦)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
67 | 63, 66 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π§ = β¨π₯, π¦β© β ((πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)))) |
68 | 55, 57 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (π§ = β¨π₯, π¦β© β ((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) = ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦))) |
69 | 68, 61 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π§ = β¨π₯, π¦β© β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)) = (((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)) βm (π₯π»π¦))) |
70 | 51, 69 | eleq12d 2828 |
. . . . . . . . . . . 12
β’ (π§ = β¨π₯, π¦β© β ((πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)) β (π₯πΊπ¦) β (((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)) βm (π₯π»π¦)))) |
71 | | ovex 7391 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)) β V |
72 | 71, 65 | elmap 8812 |
. . . . . . . . . . . 12
β’ ((π₯πΊπ¦) β (((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)) βm (π₯π»π¦)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦))) |
73 | 70, 72 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π§ = β¨π₯, π¦β© β ((πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)))) |
74 | 67, 73 | bibi12d 346 |
. . . . . . . . . 10
β’ (π§ = β¨π₯, π¦β© β (((πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β (πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§))) β ((π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦))))) |
75 | 74 | ralxp 5798 |
. . . . . . . . 9
β’
(βπ§ β
(π΄ Γ π΄)((πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β (πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§))) β βπ₯ β π΄ βπ¦ β π΄ ((π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β (π₯πΊπ¦):(π₯π»π¦)βΆ((πΉβπ₯)(Hom β(π· βΎcat π
))(πΉβπ¦)))) |
76 | 48, 75 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ πΆ β Cat) β βπ§ β (π΄ Γ π΄)((πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β (πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)))) |
77 | | ralbi 3103 |
. . . . . . . 8
β’
(βπ§ β
(π΄ Γ π΄)((πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β (πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§))) β (βπ§ β (π΄ Γ π΄)(πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β βπ§ β (π΄ Γ π΄)(πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)))) |
78 | 76, 77 | syl 17 |
. . . . . . 7
β’ ((π β§ πΆ β Cat) β (βπ§ β (π΄ Γ π΄)(πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β βπ§ β (π΄ Γ π΄)(πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)))) |
79 | 78 | 3anbi3d 1443 |
. . . . . 6
β’ ((π β§ πΆ β Cat) β ((πΊ β V β§ πΊ Fn (π΄ Γ π΄) β§ βπ§ β (π΄ Γ π΄)(πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§))) β (πΊ β V β§ πΊ Fn (π΄ Γ π΄) β§ βπ§ β (π΄ Γ π΄)(πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§))))) |
80 | | elixp2 8842 |
. . . . . 6
β’ (πΊ β Xπ§ β
(π΄ Γ π΄)(((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β (πΊ β V β§ πΊ Fn (π΄ Γ π΄) β§ βπ§ β (π΄ Γ π΄)(πΊβπ§) β (((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)))) |
81 | | elixp2 8842 |
. . . . . 6
β’ (πΊ β Xπ§ β
(π΄ Γ π΄)(((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)) β (πΊ β V β§ πΊ Fn (π΄ Γ π΄) β§ βπ§ β (π΄ Γ π΄)(πΊβπ§) β (((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)))) |
82 | 79, 80, 81 | 3bitr4g 314 |
. . . . 5
β’ ((π β§ πΆ β Cat) β (πΊ β Xπ§ β (π΄ Γ π΄)(((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β πΊ β Xπ§ β (π΄ Γ π΄)(((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)))) |
83 | 12 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β π
β (Subcatβπ·)) |
84 | 13 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β π
Fn (π Γ π)) |
85 | | eqid 2733 |
. . . . . . . . 9
β’
(Idβπ·) =
(Idβπ·) |
86 | 11 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΆ β Cat) β πΉ:π΄βΆπ) |
87 | 86 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β (πΉβπ₯) β π) |
88 | 17, 83, 84, 85, 87 | subcid 17738 |
. . . . . . . 8
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β ((Idβπ·)β(πΉβπ₯)) = ((Idβ(π· βΎcat π
))β(πΉβπ₯))) |
89 | 88 | eqeq2d 2744 |
. . . . . . 7
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β (((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβπ·)β(πΉβπ₯)) β ((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβ(π· βΎcat π
))β(πΉβπ₯)))) |
90 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(compβπ·) =
(compβπ·) |
91 | 17, 14, 19, 13, 15, 90 | rescco 17721 |
. . . . . . . . . . . . 13
β’ (π β (compβπ·) = (compβ(π· βΎcat π
))) |
92 | 91 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β (compβπ·) = (compβ(π· βΎcat π
))) |
93 | 92 | oveqd 7375 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β (β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§)) = (β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))) |
94 | 93 | oveqd 7375 |
. . . . . . . . . 10
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§))((π₯πΊπ¦)βπ)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))((π₯πΊπ¦)βπ))) |
95 | 94 | eqeq2d 2744 |
. . . . . . . . 9
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β (((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§))((π₯πΊπ¦)βπ)) β ((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))((π₯πΊπ¦)βπ)))) |
96 | 95 | 2ralbidv 3209 |
. . . . . . . 8
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β (βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§))((π₯πΊπ¦)βπ)) β βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))((π₯πΊπ¦)βπ)))) |
97 | 96 | 2ralbidv 3209 |
. . . . . . 7
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β (βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§))((π₯πΊπ¦)βπ)) β βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))((π₯πΊπ¦)βπ)))) |
98 | 89, 97 | anbi12d 632 |
. . . . . 6
β’ (((π β§ πΆ β Cat) β§ π₯ β π΄) β ((((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβπ·)β(πΉβπ₯)) β§ βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§))((π₯πΊπ¦)βπ))) β (((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβ(π· βΎcat π
))β(πΉβπ₯)) β§ βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))((π₯πΊπ¦)βπ))))) |
99 | 98 | ralbidva 3169 |
. . . . 5
β’ ((π β§ πΆ β Cat) β (βπ₯ β π΄ (((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβπ·)β(πΉβπ₯)) β§ βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§))((π₯πΊπ¦)βπ))) β βπ₯ β π΄ (((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβ(π· βΎcat π
))β(πΉβπ₯)) β§ βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))((π₯πΊπ¦)βπ))))) |
100 | 24, 82, 99 | 3anbi123d 1437 |
. . . 4
β’ ((π β§ πΆ β Cat) β ((πΉ:π΄βΆ(Baseβπ·) β§ πΊ β Xπ§ β (π΄ Γ π΄)(((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β§ βπ₯ β π΄ (((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβπ·)β(πΉβπ₯)) β§ βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§))((π₯πΊπ¦)βπ)))) β (πΉ:π΄βΆ(Baseβ(π· βΎcat π
)) β§ πΊ β Xπ§ β (π΄ Γ π΄)(((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)) β§ βπ₯ β π΄ (((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβ(π· βΎcat π
))β(πΉβπ₯)) β§ βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))((π₯πΊπ¦)βπ)))))) |
101 | | funcres2b.a |
. . . . 5
β’ π΄ = (BaseβπΆ) |
102 | | funcres2b.h |
. . . . 5
β’ π» = (Hom βπΆ) |
103 | | eqid 2733 |
. . . . 5
β’
(IdβπΆ) =
(IdβπΆ) |
104 | | eqid 2733 |
. . . . 5
β’
(compβπΆ) =
(compβπΆ) |
105 | | simpr 486 |
. . . . 5
β’ ((π β§ πΆ β Cat) β πΆ β Cat) |
106 | 19 | adantr 482 |
. . . . 5
β’ ((π β§ πΆ β Cat) β π· β Cat) |
107 | 101, 14, 102, 30, 103, 85, 104, 90, 105, 106 | isfunc 17755 |
. . . 4
β’ ((π β§ πΆ β Cat) β (πΉ(πΆ Func π·)πΊ β (πΉ:π΄βΆ(Baseβπ·) β§ πΊ β Xπ§ β (π΄ Γ π΄)(((πΉβ(1st βπ§))(Hom βπ·)(πΉβ(2nd βπ§))) βm (π»βπ§)) β§ βπ₯ β π΄ (((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβπ·)β(πΉβπ₯)) β§ βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβπ·)(πΉβπ§))((π₯πΊπ¦)βπ)))))) |
108 | | eqid 2733 |
. . . . 5
β’
(Baseβ(π·
βΎcat π
)) =
(Baseβ(π·
βΎcat π
)) |
109 | | eqid 2733 |
. . . . 5
β’ (Hom
β(π·
βΎcat π
)) =
(Hom β(π·
βΎcat π
)) |
110 | | eqid 2733 |
. . . . 5
β’
(Idβ(π·
βΎcat π
)) =
(Idβ(π·
βΎcat π
)) |
111 | | eqid 2733 |
. . . . 5
β’
(compβ(π·
βΎcat π
)) =
(compβ(π·
βΎcat π
)) |
112 | 17, 12 | subccat 17739 |
. . . . . 6
β’ (π β (π· βΎcat π
) β Cat) |
113 | 112 | adantr 482 |
. . . . 5
β’ ((π β§ πΆ β Cat) β (π· βΎcat π
) β Cat) |
114 | 101, 108,
102, 109, 103, 110, 104, 111, 105, 113 | isfunc 17755 |
. . . 4
β’ ((π β§ πΆ β Cat) β (πΉ(πΆ Func (π· βΎcat π
))πΊ β (πΉ:π΄βΆ(Baseβ(π· βΎcat π
)) β§ πΊ β Xπ§ β (π΄ Γ π΄)(((πΉβ(1st βπ§))(Hom β(π· βΎcat π
))(πΉβ(2nd βπ§))) βm (π»βπ§)) β§ βπ₯ β π΄ (((π₯πΊπ₯)β((IdβπΆ)βπ₯)) = ((Idβ(π· βΎcat π
))β(πΉβπ₯)) β§ βπ¦ β π΄ βπ§ β π΄ βπ β (π₯π»π¦)βπ β (π¦π»π§)((π₯πΊπ§)β(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (((π¦πΊπ§)βπ)(β¨(πΉβπ₯), (πΉβπ¦)β©(compβ(π· βΎcat π
))(πΉβπ§))((π₯πΊπ¦)βπ)))))) |
115 | 100, 107,
114 | 3bitr4d 311 |
. . 3
β’ ((π β§ πΆ β Cat) β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func (π· βΎcat π
))πΊ)) |
116 | 115 | ex 414 |
. 2
β’ (π β (πΆ β Cat β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func (π· βΎcat π
))πΊ))) |
117 | 5, 10, 116 | pm5.21ndd 381 |
1
β’ (π β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func (π· βΎcat π
))πΊ)) |