Step | Hyp | Ref
| Expression |
1 | | resscatc.d |
. . . . . 6
β’ π· = (CatCatβπ) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ·) =
(Baseβπ·) |
3 | | resscatc.1 |
. . . . . . . 8
β’ (π β π β π) |
4 | | resscatc.2 |
. . . . . . . 8
β’ (π β π β π) |
5 | 3, 4 | ssexd 5282 |
. . . . . . 7
β’ (π β π β V) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β π β V) |
7 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπ·) = (Hom
βπ·) |
8 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β π₯ β (π β© Cat)) |
9 | 1, 2, 5 | catcbas 17992 |
. . . . . . . 8
β’ (π β (Baseβπ·) = (π β© Cat)) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β (Baseβπ·) = (π β© Cat)) |
11 | 8, 10 | eleqtrrd 2837 |
. . . . . 6
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β π₯ β (Baseβπ·)) |
12 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β π¦ β (π β© Cat)) |
13 | 12, 10 | eleqtrrd 2837 |
. . . . . 6
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β π¦ β (Baseβπ·)) |
14 | 1, 2, 6, 7, 11, 13 | catchom 17994 |
. . . . 5
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β (π₯(Hom βπ·)π¦) = (π₯ Func π¦)) |
15 | | resscatc.c |
. . . . . 6
β’ πΆ = (CatCatβπ) |
16 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΆ) =
(BaseβπΆ) |
17 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β π β π) |
18 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
19 | | inass 4180 |
. . . . . . . . . . 11
β’ ((π β© π) β© Cat) = (π β© (π β© Cat)) |
20 | 15, 16, 3 | catcbas 17992 |
. . . . . . . . . . . 12
β’ (π β (BaseβπΆ) = (π β© Cat)) |
21 | 20 | ineq2d 4173 |
. . . . . . . . . . 11
β’ (π β (π β© (BaseβπΆ)) = (π β© (π β© Cat))) |
22 | 19, 21 | eqtr4id 2792 |
. . . . . . . . . 10
β’ (π β ((π β© π) β© Cat) = (π β© (BaseβπΆ))) |
23 | | df-ss 3928 |
. . . . . . . . . . . 12
β’ (π β π β (π β© π) = π) |
24 | 4, 23 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π β© π) = π) |
25 | 24 | ineq1d 4172 |
. . . . . . . . . 10
β’ (π β ((π β© π) β© Cat) = (π β© Cat)) |
26 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (πΆ βΎs π) = (πΆ βΎs π) |
27 | 26, 16 | ressbas 17123 |
. . . . . . . . . . 11
β’ (π β V β (π β© (BaseβπΆ)) = (Baseβ(πΆ βΎs π))) |
28 | 5, 27 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β© (BaseβπΆ)) = (Baseβ(πΆ βΎs π))) |
29 | 22, 25, 28 | 3eqtr3d 2781 |
. . . . . . . . 9
β’ (π β (π β© Cat) = (Baseβ(πΆ βΎs π))) |
30 | 26, 16 | ressbasss 17126 |
. . . . . . . . 9
β’
(Baseβ(πΆ
βΎs π))
β (BaseβπΆ) |
31 | 29, 30 | eqsstrdi 3999 |
. . . . . . . 8
β’ (π β (π β© Cat) β (BaseβπΆ)) |
32 | 31 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β (π β© Cat) β (BaseβπΆ)) |
33 | 32, 8 | sseldd 3946 |
. . . . . 6
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β π₯ β (BaseβπΆ)) |
34 | 32, 12 | sseldd 3946 |
. . . . . 6
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β π¦ β (BaseβπΆ)) |
35 | 15, 16, 17, 18, 33, 34 | catchom 17994 |
. . . . 5
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β (π₯(Hom βπΆ)π¦) = (π₯ Func π¦)) |
36 | 26, 18 | resshom 17305 |
. . . . . . 7
β’ (π β V β (Hom
βπΆ) = (Hom
β(πΆ
βΎs π))) |
37 | 5, 36 | syl 17 |
. . . . . 6
β’ (π β (Hom βπΆ) = (Hom β(πΆ βΎs π))) |
38 | 37 | oveqdr 7386 |
. . . . 5
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β (π₯(Hom βπΆ)π¦) = (π₯(Hom β(πΆ βΎs π))π¦)) |
39 | 14, 35, 38 | 3eqtr2rd 2780 |
. . . 4
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat))) β (π₯(Hom β(πΆ βΎs π))π¦) = (π₯(Hom βπ·)π¦)) |
40 | 39 | ralrimivva 3194 |
. . 3
β’ (π β βπ₯ β (π β© Cat)βπ¦ β (π β© Cat)(π₯(Hom β(πΆ βΎs π))π¦) = (π₯(Hom βπ·)π¦)) |
41 | | eqid 2733 |
. . . 4
β’ (Hom
β(πΆ
βΎs π)) =
(Hom β(πΆ
βΎs π)) |
42 | 9 | eqcomd 2739 |
. . . 4
β’ (π β (π β© Cat) = (Baseβπ·)) |
43 | 41, 7, 29, 42 | homfeq 17579 |
. . 3
β’ (π β ((Homf
β(πΆ
βΎs π)) =
(Homf βπ·) β βπ₯ β (π β© Cat)βπ¦ β (π β© Cat)(π₯(Hom β(πΆ βΎs π))π¦) = (π₯(Hom βπ·)π¦))) |
44 | 40, 43 | mpbird 257 |
. 2
β’ (π β (Homf
β(πΆ
βΎs π)) =
(Homf βπ·)) |
45 | 5 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β V) |
46 | | eqid 2733 |
. . . . . . . 8
β’
(compβπ·) =
(compβπ·) |
47 | | simplr1 1216 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π₯ β (π β© Cat)) |
48 | 9 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (Baseβπ·) = (π β© Cat)) |
49 | 47, 48 | eleqtrrd 2837 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π₯ β (Baseβπ·)) |
50 | | simplr2 1217 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π¦ β (π β© Cat)) |
51 | 50, 48 | eleqtrrd 2837 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π¦ β (Baseβπ·)) |
52 | | simplr3 1218 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π§ β (π β© Cat)) |
53 | 52, 48 | eleqtrrd 2837 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π§ β (Baseβπ·)) |
54 | | simprl 770 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β (π₯(Hom βπ·)π¦)) |
55 | 1, 2, 45, 7, 49, 51 | catchom 17994 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π₯(Hom βπ·)π¦) = (π₯ Func π¦)) |
56 | 54, 55 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β (π₯ Func π¦)) |
57 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β (π¦(Hom βπ·)π§)) |
58 | 1, 2, 45, 7, 51, 53 | catchom 17994 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π¦(Hom βπ·)π§) = (π¦ Func π§)) |
59 | 57, 58 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β (π¦ Func π§)) |
60 | 1, 2, 45, 46, 49, 51, 53, 56, 59 | catcco 17996 |
. . . . . . 7
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π(β¨π₯, π¦β©(compβπ·)π§)π) = (π βfunc π)) |
61 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β π) |
62 | | eqid 2733 |
. . . . . . . 8
β’
(compβπΆ) =
(compβπΆ) |
63 | 31 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π β© Cat) β (BaseβπΆ)) |
64 | 63, 47 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π₯ β (BaseβπΆ)) |
65 | 63, 50 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π¦ β (BaseβπΆ)) |
66 | 63, 52 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π§ β (BaseβπΆ)) |
67 | 15, 16, 61, 62, 64, 65, 66, 56, 59 | catcco 17996 |
. . . . . . 7
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) = (π βfunc π)) |
68 | 26, 62 | ressco 17306 |
. . . . . . . . . . 11
β’ (π β V β
(compβπΆ) =
(compβ(πΆ
βΎs π))) |
69 | 5, 68 | syl 17 |
. . . . . . . . . 10
β’ (π β (compβπΆ) = (compβ(πΆ βΎs π))) |
70 | 69 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (compβπΆ) = (compβ(πΆ βΎs π))) |
71 | 70 | oveqd 7375 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (β¨π₯, π¦β©(compβπΆ)π§) = (β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)) |
72 | 71 | oveqd 7375 |
. . . . . . 7
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π)) |
73 | 60, 67, 72 | 3eqtr2d 2779 |
. . . . . 6
β’ (((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π(β¨π₯, π¦β©(compβπ·)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π)) |
74 | 73 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ (π₯ β (π β© Cat) β§ π¦ β (π β© Cat) β§ π§ β (π β© Cat))) β βπ β (π₯(Hom βπ·)π¦)βπ β (π¦(Hom βπ·)π§)(π(β¨π₯, π¦β©(compβπ·)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π)) |
75 | 74 | ralrimivvva 3197 |
. . . 4
β’ (π β βπ₯ β (π β© Cat)βπ¦ β (π β© Cat)βπ§ β (π β© Cat)βπ β (π₯(Hom βπ·)π¦)βπ β (π¦(Hom βπ·)π§)(π(β¨π₯, π¦β©(compβπ·)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π)) |
76 | | eqid 2733 |
. . . . 5
β’
(compβ(πΆ
βΎs π)) =
(compβ(πΆ
βΎs π)) |
77 | 44 | eqcomd 2739 |
. . . . 5
β’ (π β (Homf
βπ·) =
(Homf β(πΆ βΎs π))) |
78 | 46, 76, 7, 42, 29, 77 | comfeq 17591 |
. . . 4
β’ (π β
((compfβπ·) = (compfβ(πΆ βΎs π)) β βπ₯ β (π β© Cat)βπ¦ β (π β© Cat)βπ§ β (π β© Cat)βπ β (π₯(Hom βπ·)π¦)βπ β (π¦(Hom βπ·)π§)(π(β¨π₯, π¦β©(compβπ·)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π))) |
79 | 75, 78 | mpbird 257 |
. . 3
β’ (π β
(compfβπ·) = (compfβ(πΆ βΎs π))) |
80 | 79 | eqcomd 2739 |
. 2
β’ (π β
(compfβ(πΆ βΎs π)) = (compfβπ·)) |
81 | 44, 80 | jca 513 |
1
β’ (π β ((Homf
β(πΆ
βΎs π)) =
(Homf βπ·) β§
(compfβ(πΆ βΎs π)) = (compfβπ·))) |