Step | Hyp | Ref
| Expression |
1 | | resssetc.d |
. . . . . 6
β’ π· = (SetCatβπ) |
2 | | resssetc.1 |
. . . . . . . 8
β’ (π β π β π) |
3 | | resssetc.2 |
. . . . . . . 8
β’ (π β π β π) |
4 | 2, 3 | ssexd 5282 |
. . . . . . 7
β’ (π β π β V) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π β V) |
6 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπ·) = (Hom
βπ·) |
7 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
8 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
9 | 1, 5, 6, 7, 8 | setchom 17971 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(Hom βπ·)π¦) = (π¦ βm π₯)) |
10 | | resssetc.c |
. . . . . 6
β’ πΆ = (SetCatβπ) |
11 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π β π) |
12 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
13 | 3 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π β π) |
14 | 13, 7 | sseldd 3946 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
15 | 13, 8 | sseldd 3946 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
16 | 10, 11, 12, 14, 15 | setchom 17971 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(Hom βπΆ)π¦) = (π¦ βm π₯)) |
17 | | eqid 2733 |
. . . . . . . 8
β’ (πΆ βΎs π) = (πΆ βΎs π) |
18 | 17, 12 | resshom 17305 |
. . . . . . 7
β’ (π β V β (Hom
βπΆ) = (Hom
β(πΆ
βΎs π))) |
19 | 4, 18 | syl 17 |
. . . . . 6
β’ (π β (Hom βπΆ) = (Hom β(πΆ βΎs π))) |
20 | 19 | oveqdr 7386 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(Hom βπΆ)π¦) = (π₯(Hom β(πΆ βΎs π))π¦)) |
21 | 9, 16, 20 | 3eqtr2rd 2780 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(Hom β(πΆ βΎs π))π¦) = (π₯(Hom βπ·)π¦)) |
22 | 21 | ralrimivva 3194 |
. . 3
β’ (π β βπ₯ β π βπ¦ β π (π₯(Hom β(πΆ βΎs π))π¦) = (π₯(Hom βπ·)π¦)) |
23 | | eqid 2733 |
. . . 4
β’ (Hom
β(πΆ
βΎs π)) =
(Hom β(πΆ
βΎs π)) |
24 | 10, 2 | setcbas 17969 |
. . . . . 6
β’ (π β π = (BaseβπΆ)) |
25 | 3, 24 | sseqtrd 3985 |
. . . . 5
β’ (π β π β (BaseβπΆ)) |
26 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΆ) =
(BaseβπΆ) |
27 | 17, 26 | ressbas2 17125 |
. . . . 5
β’ (π β (BaseβπΆ) β π = (Baseβ(πΆ βΎs π))) |
28 | 25, 27 | syl 17 |
. . . 4
β’ (π β π = (Baseβ(πΆ βΎs π))) |
29 | 1, 4 | setcbas 17969 |
. . . 4
β’ (π β π = (Baseβπ·)) |
30 | 23, 6, 28, 29 | homfeq 17579 |
. . 3
β’ (π β ((Homf
β(πΆ
βΎs π)) =
(Homf βπ·) β βπ₯ β π βπ¦ β π (π₯(Hom β(πΆ βΎs π))π¦) = (π₯(Hom βπ·)π¦))) |
31 | 22, 30 | mpbird 257 |
. 2
β’ (π β (Homf
β(πΆ
βΎs π)) =
(Homf βπ·)) |
32 | 4 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β V) |
33 | | eqid 2733 |
. . . . . . . 8
β’
(compβπ·) =
(compβπ·) |
34 | | simplr1 1216 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π₯ β π) |
35 | | simplr2 1217 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π¦ β π) |
36 | | simplr3 1218 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π§ β π) |
37 | | simprl 770 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β (π₯(Hom βπ·)π¦)) |
38 | 1, 32, 6, 34, 35 | elsetchom 17972 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π β (π₯(Hom βπ·)π¦) β π:π₯βΆπ¦)) |
39 | 37, 38 | mpbid 231 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π:π₯βΆπ¦) |
40 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β (π¦(Hom βπ·)π§)) |
41 | 1, 32, 6, 35, 36 | elsetchom 17972 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π β (π¦(Hom βπ·)π§) β π:π¦βΆπ§)) |
42 | 40, 41 | mpbid 231 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π:π¦βΆπ§) |
43 | 1, 32, 33, 34, 35, 36, 39, 42 | setcco 17974 |
. . . . . . 7
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π(β¨π₯, π¦β©(compβπ·)π§)π) = (π β π)) |
44 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β π) |
45 | | eqid 2733 |
. . . . . . . 8
β’
(compβπΆ) =
(compβπΆ) |
46 | 3 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π β π) |
47 | 46, 34 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π₯ β π) |
48 | 46, 35 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π¦ β π) |
49 | 46, 36 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β π§ β π) |
50 | 10, 44, 45, 47, 48, 49, 39, 42 | setcco 17974 |
. . . . . . 7
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) = (π β π)) |
51 | 17, 45 | ressco 17306 |
. . . . . . . . . . 11
β’ (π β V β
(compβπΆ) =
(compβ(πΆ
βΎs π))) |
52 | 4, 51 | syl 17 |
. . . . . . . . . 10
β’ (π β (compβπΆ) = (compβ(πΆ βΎs π))) |
53 | 52 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (compβπΆ) = (compβ(πΆ βΎs π))) |
54 | 53 | oveqd 7375 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (β¨π₯, π¦β©(compβπΆ)π§) = (β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)) |
55 | 54 | oveqd 7375 |
. . . . . . 7
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π)) |
56 | 43, 50, 55 | 3eqtr2d 2779 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯(Hom βπ·)π¦) β§ π β (π¦(Hom βπ·)π§))) β (π(β¨π₯, π¦β©(compβπ·)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π)) |
57 | 56 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β βπ β (π₯(Hom βπ·)π¦)βπ β (π¦(Hom βπ·)π§)(π(β¨π₯, π¦β©(compβπ·)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π)) |
58 | 57 | ralrimivvva 3197 |
. . . 4
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π βπ β (π₯(Hom βπ·)π¦)βπ β (π¦(Hom βπ·)π§)(π(β¨π₯, π¦β©(compβπ·)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π)) |
59 | | eqid 2733 |
. . . . 5
β’
(compβ(πΆ
βΎs π)) =
(compβ(πΆ
βΎs π)) |
60 | 31 | eqcomd 2739 |
. . . . 5
β’ (π β (Homf
βπ·) =
(Homf β(πΆ βΎs π))) |
61 | 33, 59, 6, 29, 28, 60 | comfeq 17591 |
. . . 4
β’ (π β
((compfβπ·) = (compfβ(πΆ βΎs π)) β βπ₯ β π βπ¦ β π βπ§ β π βπ β (π₯(Hom βπ·)π¦)βπ β (π¦(Hom βπ·)π§)(π(β¨π₯, π¦β©(compβπ·)π§)π) = (π(β¨π₯, π¦β©(compβ(πΆ βΎs π))π§)π))) |
62 | 58, 61 | mpbird 257 |
. . 3
β’ (π β
(compfβπ·) = (compfβ(πΆ βΎs π))) |
63 | 62 | eqcomd 2739 |
. 2
β’ (π β
(compfβ(πΆ βΎs π)) = (compfβπ·)) |
64 | 31, 63 | jca 513 |
1
β’ (π β ((Homf
β(πΆ
βΎs π)) =
(Homf βπ·) β§
(compfβ(πΆ βΎs π)) = (compfβπ·))) |