Step | Hyp | Ref
| Expression |
1 | | oveq2 7413 |
. . . . . . . 8
β’ (π = π β (π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π) = (π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)) |
2 | 1 | oveq1d 7420 |
. . . . . . 7
β’ (π = π β ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ)) = ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))) |
3 | 2 | fveq1d 6890 |
. . . . . 6
β’ (π = π β (((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ) = (((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)) |
4 | 3 | fveq1d 6890 |
. . . . 5
β’ (π = π β ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ)) = ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ))) |
5 | 4 | cbvmptv 5260 |
. . . 4
β’ (π β (((1st
βπ)βπ)(π Nat π)πΉ) β¦ ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ))) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ))) |
6 | | yoneda.q |
. . . . . . . . 9
β’ π = (π FuncCat π) |
7 | | eqid 2732 |
. . . . . . . . 9
β’ (π Nat π) = (π Nat π) |
8 | | yoneda.o |
. . . . . . . . . 10
β’ π = (oppCatβπΆ) |
9 | | yoneda.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΆ) |
10 | 8, 9 | oppcbas 17659 |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
11 | | eqid 2732 |
. . . . . . . . 9
β’
(compβπ) =
(compβπ) |
12 | | eqid 2732 |
. . . . . . . . 9
β’
(compβπ) =
(compβπ) |
13 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (Hom
βπΆ) = (Hom
βπΆ) |
14 | 6, 7 | fuchom 17909 |
. . . . . . . . . . . 12
β’ (π Nat π) = (Hom βπ) |
15 | | relfunc 17808 |
. . . . . . . . . . . . 13
β’ Rel
(πΆ Func π) |
16 | | yoneda.y |
. . . . . . . . . . . . . 14
β’ π = (YonβπΆ) |
17 | | yoneda.c |
. . . . . . . . . . . . . 14
β’ (π β πΆ β Cat) |
18 | | yoneda.s |
. . . . . . . . . . . . . 14
β’ π = (SetCatβπ) |
19 | | yoneda.w |
. . . . . . . . . . . . . . 15
β’ (π β π β π) |
20 | | yoneda.v |
. . . . . . . . . . . . . . . 16
β’ (π β (ran
(Homf βπ) βͺ π) β π) |
21 | 20 | unssbd 4187 |
. . . . . . . . . . . . . . 15
β’ (π β π β π) |
22 | 19, 21 | ssexd 5323 |
. . . . . . . . . . . . . 14
β’ (π β π β V) |
23 | | yoneda.u |
. . . . . . . . . . . . . 14
β’ (π β ran
(Homf βπΆ) β π) |
24 | 16, 17, 8, 18, 6, 22, 23 | yoncl 18211 |
. . . . . . . . . . . . 13
β’ (π β π β (πΆ Func π)) |
25 | | 1st2ndbr 8024 |
. . . . . . . . . . . . 13
β’ ((Rel
(πΆ Func π) β§ π β (πΆ Func π)) β (1st βπ)(πΆ Func π)(2nd βπ)) |
26 | 15, 24, 25 | sylancr 587 |
. . . . . . . . . . . 12
β’ (π β (1st
βπ)(πΆ Func π)(2nd βπ)) |
27 | | yonedalem22.p |
. . . . . . . . . . . 12
β’ (π β π β π΅) |
28 | | yonedalem21.x |
. . . . . . . . . . . 12
β’ (π β π β π΅) |
29 | 9, 13, 14, 26, 27, 28 | funcf2 17814 |
. . . . . . . . . . 11
β’ (π β (π(2nd βπ)π):(π(Hom βπΆ)π)βΆ(((1st βπ)βπ)(π Nat π)((1st βπ)βπ))) |
30 | | yonedalem22.k |
. . . . . . . . . . 11
β’ (π β πΎ β (π(Hom βπΆ)π)) |
31 | 29, 30 | ffvelcdmd 7084 |
. . . . . . . . . 10
β’ (π β ((π(2nd βπ)π)βπΎ) β (((1st βπ)βπ)(π Nat π)((1st βπ)βπ))) |
32 | 31 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((π(2nd βπ)π)βπΎ) β (((1st βπ)βπ)(π Nat π)((1st βπ)βπ))) |
33 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β (((1st βπ)βπ)(π Nat π)πΉ)) |
34 | | yonedalem22.a |
. . . . . . . . . . 11
β’ (π β π΄ β (πΉ(π Nat π)πΊ)) |
35 | 34 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π΄ β (πΉ(π Nat π)πΊ)) |
36 | 6, 7, 12, 33, 35 | fuccocl 17913 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π) β (((1st βπ)βπ)(π Nat π)πΊ)) |
37 | 27 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β π΅) |
38 | 6, 7, 10, 11, 12, 32, 36, 37 | fuccoval 17912 |
. . . . . . . 8
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ) = (((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)βπ)(β¨((1st
β((1st βπ)βπ))βπ), ((1st β((1st
βπ)βπ))βπ)β©(compβπ)((1st βπΊ)βπ))(((π(2nd βπ)π)βπΎ)βπ))) |
39 | 6, 7, 10, 11, 12, 33, 35, 37 | fuccoval 17912 |
. . . . . . . . . 10
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)βπ) = ((π΄βπ)(β¨((1st
β((1st βπ)βπ))βπ), ((1st βπΉ)βπ)β©(compβπ)((1st βπΊ)βπ))(πβπ))) |
40 | 22 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β V) |
41 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ) =
(Baseβπ) |
42 | | relfunc 17808 |
. . . . . . . . . . . . . . . 16
β’ Rel
(π Func π) |
43 | 6 | fucbas 17908 |
. . . . . . . . . . . . . . . . . 18
β’ (π Func π) = (Baseβπ) |
44 | 9, 43, 26 | funcf1 17812 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1st
βπ):π΅βΆ(π Func π)) |
45 | 44, 28 | ffvelcdmd 7084 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1st
βπ)βπ) β (π Func π)) |
46 | | 1st2ndbr 8024 |
. . . . . . . . . . . . . . . 16
β’ ((Rel
(π Func π) β§ ((1st βπ)βπ) β (π Func π)) β (1st
β((1st βπ)βπ))(π Func π)(2nd β((1st
βπ)βπ))) |
47 | 42, 45, 46 | sylancr 587 |
. . . . . . . . . . . . . . 15
β’ (π β (1st
β((1st βπ)βπ))(π Func π)(2nd β((1st
βπ)βπ))) |
48 | 10, 41, 47 | funcf1 17812 |
. . . . . . . . . . . . . 14
β’ (π β (1st
β((1st βπ)βπ)):π΅βΆ(Baseβπ)) |
49 | 18, 22 | setcbas 18024 |
. . . . . . . . . . . . . . 15
β’ (π β π = (Baseβπ)) |
50 | 49 | feq3d 6701 |
. . . . . . . . . . . . . 14
β’ (π β ((1st
β((1st βπ)βπ)):π΅βΆπ β (1st
β((1st βπ)βπ)):π΅βΆ(Baseβπ))) |
51 | 48, 50 | mpbird 256 |
. . . . . . . . . . . . 13
β’ (π β (1st
β((1st βπ)βπ)):π΅βΆπ) |
52 | 51, 27 | ffvelcdmd 7084 |
. . . . . . . . . . . 12
β’ (π β ((1st
β((1st βπ)βπ))βπ) β π) |
53 | 52 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((1st
β((1st βπ)βπ))βπ) β π) |
54 | | yonedalem21.f |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ β (π Func π)) |
55 | | 1st2ndbr 8024 |
. . . . . . . . . . . . . . . 16
β’ ((Rel
(π Func π) β§ πΉ β (π Func π)) β (1st βπΉ)(π Func π)(2nd βπΉ)) |
56 | 42, 54, 55 | sylancr 587 |
. . . . . . . . . . . . . . 15
β’ (π β (1st
βπΉ)(π Func π)(2nd βπΉ)) |
57 | 10, 41, 56 | funcf1 17812 |
. . . . . . . . . . . . . 14
β’ (π β (1st
βπΉ):π΅βΆ(Baseβπ)) |
58 | 49 | feq3d 6701 |
. . . . . . . . . . . . . 14
β’ (π β ((1st
βπΉ):π΅βΆπ β (1st βπΉ):π΅βΆ(Baseβπ))) |
59 | 57, 58 | mpbird 256 |
. . . . . . . . . . . . 13
β’ (π β (1st
βπΉ):π΅βΆπ) |
60 | 59, 27 | ffvelcdmd 7084 |
. . . . . . . . . . . 12
β’ (π β ((1st
βπΉ)βπ) β π) |
61 | 60 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((1st βπΉ)βπ) β π) |
62 | | yonedalem22.g |
. . . . . . . . . . . . . . . 16
β’ (π β πΊ β (π Func π)) |
63 | | 1st2ndbr 8024 |
. . . . . . . . . . . . . . . 16
β’ ((Rel
(π Func π) β§ πΊ β (π Func π)) β (1st βπΊ)(π Func π)(2nd βπΊ)) |
64 | 42, 62, 63 | sylancr 587 |
. . . . . . . . . . . . . . 15
β’ (π β (1st
βπΊ)(π Func π)(2nd βπΊ)) |
65 | 10, 41, 64 | funcf1 17812 |
. . . . . . . . . . . . . 14
β’ (π β (1st
βπΊ):π΅βΆ(Baseβπ)) |
66 | 65, 27 | ffvelcdmd 7084 |
. . . . . . . . . . . . 13
β’ (π β ((1st
βπΊ)βπ) β (Baseβπ)) |
67 | 66, 49 | eleqtrrd 2836 |
. . . . . . . . . . . 12
β’ (π β ((1st
βπΊ)βπ) β π) |
68 | 67 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((1st βπΊ)βπ) β π) |
69 | 7, 33 | nat1st2nd 17898 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β (β¨(1st
β((1st βπ)βπ)), (2nd β((1st
βπ)βπ))β©(π Nat π)β¨(1st βπΉ), (2nd βπΉ)β©)) |
70 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ (Hom
βπ) = (Hom
βπ) |
71 | 7, 69, 10, 70, 37 | natcl 17900 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (πβπ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st βπΉ)βπ))) |
72 | 18, 40, 70, 53, 61 | elsetchom 18027 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st βπΉ)βπ)) β (πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ))) |
73 | 71, 72 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ)) |
74 | 7, 34 | nat1st2nd 17898 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (β¨(1st βπΉ), (2nd βπΉ)β©(π Nat π)β¨(1st βπΊ), (2nd βπΊ)β©)) |
75 | 7, 74, 10, 70, 27 | natcl 17900 |
. . . . . . . . . . . . 13
β’ (π β (π΄βπ) β (((1st βπΉ)βπ)(Hom βπ)((1st βπΊ)βπ))) |
76 | 18, 22, 70, 60, 67 | elsetchom 18027 |
. . . . . . . . . . . . 13
β’ (π β ((π΄βπ) β (((1st βπΉ)βπ)(Hom βπ)((1st βπΊ)βπ)) β (π΄βπ):((1st βπΉ)βπ)βΆ((1st βπΊ)βπ))) |
77 | 75, 76 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β (π΄βπ):((1st βπΉ)βπ)βΆ((1st βπΊ)βπ)) |
78 | 77 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (π΄βπ):((1st βπΉ)βπ)βΆ((1st βπΊ)βπ)) |
79 | 18, 40, 11, 53, 61, 68, 73, 78 | setcco 18029 |
. . . . . . . . . 10
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((π΄βπ)(β¨((1st
β((1st βπ)βπ))βπ), ((1st βπΉ)βπ)β©(compβπ)((1st βπΊ)βπ))(πβπ)) = ((π΄βπ) β (πβπ))) |
80 | 39, 79 | eqtrd 2772 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)βπ) = ((π΄βπ) β (πβπ))) |
81 | 80 | oveq1d 7420 |
. . . . . . . 8
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)βπ)(β¨((1st
β((1st βπ)βπ))βπ), ((1st β((1st
βπ)βπ))βπ)β©(compβπ)((1st βπΊ)βπ))(((π(2nd βπ)π)βπΎ)βπ)) = (((π΄βπ) β (πβπ))(β¨((1st
β((1st βπ)βπ))βπ), ((1st β((1st
βπ)βπ))βπ)β©(compβπ)((1st βπΊ)βπ))(((π(2nd βπ)π)βπΎ)βπ))) |
82 | 44, 27 | ffvelcdmd 7084 |
. . . . . . . . . . . . . 14
β’ (π β ((1st
βπ)βπ) β (π Func π)) |
83 | | 1st2ndbr 8024 |
. . . . . . . . . . . . . 14
β’ ((Rel
(π Func π) β§ ((1st βπ)βπ) β (π Func π)) β (1st
β((1st βπ)βπ))(π Func π)(2nd β((1st
βπ)βπ))) |
84 | 42, 82, 83 | sylancr 587 |
. . . . . . . . . . . . 13
β’ (π β (1st
β((1st βπ)βπ))(π Func π)(2nd β((1st
βπ)βπ))) |
85 | 10, 41, 84 | funcf1 17812 |
. . . . . . . . . . . 12
β’ (π β (1st
β((1st βπ)βπ)):π΅βΆ(Baseβπ)) |
86 | 85, 27 | ffvelcdmd 7084 |
. . . . . . . . . . 11
β’ (π β ((1st
β((1st βπ)βπ))βπ) β (Baseβπ)) |
87 | 86, 49 | eleqtrrd 2836 |
. . . . . . . . . 10
β’ (π β ((1st
β((1st βπ)βπ))βπ) β π) |
88 | 87 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((1st
β((1st βπ)βπ))βπ) β π) |
89 | 7, 31 | nat1st2nd 17898 |
. . . . . . . . . . . 12
β’ (π β ((π(2nd βπ)π)βπΎ) β (β¨(1st
β((1st βπ)βπ)), (2nd β((1st
βπ)βπ))β©(π Nat π)β¨(1st
β((1st βπ)βπ)), (2nd β((1st
βπ)βπ))β©)) |
90 | 7, 89, 10, 70, 27 | natcl 17900 |
. . . . . . . . . . 11
β’ (π β (((π(2nd βπ)π)βπΎ)βπ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st β((1st
βπ)βπ))βπ))) |
91 | 18, 22, 70, 87, 52 | elsetchom 18027 |
. . . . . . . . . . 11
β’ (π β ((((π(2nd βπ)π)βπΎ)βπ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st β((1st
βπ)βπ))βπ)) β (((π(2nd βπ)π)βπΎ)βπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st
β((1st βπ)βπ))βπ))) |
92 | 90, 91 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (((π(2nd βπ)π)βπΎ)βπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st
β((1st βπ)βπ))βπ)) |
93 | 92 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π(2nd βπ)π)βπΎ)βπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st
β((1st βπ)βπ))βπ)) |
94 | | fco 6738 |
. . . . . . . . . 10
β’ (((π΄βπ):((1st βπΉ)βπ)βΆ((1st βπΊ)βπ) β§ (πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ)) β ((π΄βπ) β (πβπ)):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΊ)βπ)) |
95 | 78, 73, 94 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((π΄βπ) β (πβπ)):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΊ)βπ)) |
96 | 18, 40, 11, 88, 53, 68, 93, 95 | setcco 18029 |
. . . . . . . 8
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π΄βπ) β (πβπ))(β¨((1st
β((1st βπ)βπ))βπ), ((1st β((1st
βπ)βπ))βπ)β©(compβπ)((1st βπΊ)βπ))(((π(2nd βπ)π)βπΎ)βπ)) = (((π΄βπ) β (πβπ)) β (((π(2nd βπ)π)βπΎ)βπ))) |
97 | 38, 81, 96 | 3eqtrd 2776 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ) = (((π΄βπ) β (πβπ)) β (((π(2nd βπ)π)βπΎ)βπ))) |
98 | 97 | fveq1d 6890 |
. . . . . 6
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ)) = ((((π΄βπ) β (πβπ)) β (((π(2nd βπ)π)βπΎ)βπ))β( 1 βπ))) |
99 | | yoneda.1 |
. . . . . . . . . 10
β’ 1 =
(IdβπΆ) |
100 | 9, 13, 99, 17, 27 | catidcl 17622 |
. . . . . . . . 9
β’ (π β ( 1 βπ) β (π(Hom βπΆ)π)) |
101 | 16, 9, 17, 27, 13, 27 | yon11 18213 |
. . . . . . . . 9
β’ (π β ((1st
β((1st βπ)βπ))βπ) = (π(Hom βπΆ)π)) |
102 | 100, 101 | eleqtrrd 2836 |
. . . . . . . 8
β’ (π β ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) |
103 | 102 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) |
104 | | fvco3 6987 |
. . . . . . 7
β’
(((((π(2nd βπ)π)βπΎ)βπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st
β((1st βπ)βπ))βπ) β§ ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) β ((((π΄βπ) β (πβπ)) β (((π(2nd βπ)π)βπΎ)βπ))β( 1 βπ)) = (((π΄βπ) β (πβπ))β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ)))) |
105 | 93, 103, 104 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((((π΄βπ) β (πβπ)) β (((π(2nd βπ)π)βπΎ)βπ))β( 1 βπ)) = (((π΄βπ) β (πβπ))β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ)))) |
106 | 93, 103 | ffvelcdmd 7084 |
. . . . . . . 8
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ)) β ((1st
β((1st βπ)βπ))βπ)) |
107 | | fvco3 6987 |
. . . . . . . 8
β’ (((πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ) β§ ((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ)) β ((1st
β((1st βπ)βπ))βπ)) β (((π΄βπ) β (πβπ))β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ))) = ((π΄βπ)β((πβπ)β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ))))) |
108 | 73, 106, 107 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π΄βπ) β (πβπ))β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ))) = ((π΄βπ)β((πβπ)β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ))))) |
109 | 17 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β πΆ β Cat) |
110 | 28 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β π΅) |
111 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(compβπΆ) =
(compβπΆ) |
112 | 30 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β πΎ β (π(Hom βπΆ)π)) |
113 | 100 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ( 1 βπ) β (π(Hom βπΆ)π)) |
114 | 16, 9, 109, 37, 13, 110, 111, 37, 112, 113 | yon2 18215 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ)) = (πΎ(β¨π, πβ©(compβπΆ)π)( 1 βπ))) |
115 | 9, 13, 99, 109, 37, 111, 110, 112 | catrid 17624 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (πΎ(β¨π, πβ©(compβπΆ)π)( 1 βπ)) = πΎ) |
116 | 114, 115 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ)) = πΎ) |
117 | 116 | fveq2d 6892 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ)β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ))) = ((πβπ)βπΎ)) |
118 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ (Hom
βπ) = (Hom
βπ) |
119 | 10, 118, 70, 47, 28, 27 | funcf2 17814 |
. . . . . . . . . . . . . 14
β’ (π β (π(2nd β((1st
βπ)βπ))π):(π(Hom βπ)π)βΆ(((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st β((1st
βπ)βπ))βπ))) |
120 | 13, 8 | oppchom 17656 |
. . . . . . . . . . . . . . 15
β’ (π(Hom βπ)π) = (π(Hom βπΆ)π) |
121 | 30, 120 | eleqtrrdi 2844 |
. . . . . . . . . . . . . 14
β’ (π β πΎ β (π(Hom βπ)π)) |
122 | 119, 121 | ffvelcdmd 7084 |
. . . . . . . . . . . . 13
β’ (π β ((π(2nd β((1st
βπ)βπ))π)βπΎ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st β((1st
βπ)βπ))βπ))) |
123 | 51, 28 | ffvelcdmd 7084 |
. . . . . . . . . . . . . 14
β’ (π β ((1st
β((1st βπ)βπ))βπ) β π) |
124 | 18, 22, 70, 123, 52 | elsetchom 18027 |
. . . . . . . . . . . . 13
β’ (π β (((π(2nd β((1st
βπ)βπ))π)βπΎ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st β((1st
βπ)βπ))βπ)) β ((π(2nd β((1st
βπ)βπ))π)βπΎ):((1st β((1st
βπ)βπ))βπ)βΆ((1st
β((1st βπ)βπ))βπ))) |
125 | 122, 124 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β ((π(2nd β((1st
βπ)βπ))π)βπΎ):((1st β((1st
βπ)βπ))βπ)βΆ((1st
β((1st βπ)βπ))βπ)) |
126 | 125 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((π(2nd β((1st
βπ)βπ))π)βπΎ):((1st β((1st
βπ)βπ))βπ)βΆ((1st
β((1st βπ)βπ))βπ)) |
127 | 9, 13, 99, 17, 28 | catidcl 17622 |
. . . . . . . . . . . . 13
β’ (π β ( 1 βπ) β (π(Hom βπΆ)π)) |
128 | 16, 9, 17, 28, 13, 28 | yon11 18213 |
. . . . . . . . . . . . 13
β’ (π β ((1st
β((1st βπ)βπ))βπ) = (π(Hom βπΆ)π)) |
129 | 127, 128 | eleqtrrd 2836 |
. . . . . . . . . . . 12
β’ (π β ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) |
130 | 129 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) |
131 | | fvco3 6987 |
. . . . . . . . . . 11
β’ ((((π(2nd
β((1st βπ)βπ))π)βπΎ):((1st β((1st
βπ)βπ))βπ)βΆ((1st
β((1st βπ)βπ))βπ) β§ ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) β (((πβπ) β ((π(2nd β((1st
βπ)βπ))π)βπΎ))β( 1 βπ)) = ((πβπ)β(((π(2nd β((1st
βπ)βπ))π)βπΎ)β( 1 βπ)))) |
132 | 126, 130,
131 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((πβπ) β ((π(2nd β((1st
βπ)βπ))π)βπΎ))β( 1 βπ)) = ((πβπ)β(((π(2nd β((1st
βπ)βπ))π)βπΎ)β( 1 βπ)))) |
133 | 121 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β πΎ β (π(Hom βπ)π)) |
134 | 7, 69, 10, 118, 11, 110, 37, 133 | nati 17902 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ)(β¨((1st
β((1st βπ)βπ))βπ), ((1st β((1st
βπ)βπ))βπ)β©(compβπ)((1st βπΉ)βπ))((π(2nd β((1st
βπ)βπ))π)βπΎ)) = (((π(2nd βπΉ)π)βπΎ)(β¨((1st
β((1st βπ)βπ))βπ), ((1st βπΉ)βπ)β©(compβπ)((1st βπΉ)βπ))(πβπ))) |
135 | 123 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((1st
β((1st βπ)βπ))βπ) β π) |
136 | 18, 40, 11, 135, 53, 61, 126, 73 | setcco 18029 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ)(β¨((1st
β((1st βπ)βπ))βπ), ((1st β((1st
βπ)βπ))βπ)β©(compβπ)((1st βπΉ)βπ))((π(2nd β((1st
βπ)βπ))π)βπΎ)) = ((πβπ) β ((π(2nd β((1st
βπ)βπ))π)βπΎ))) |
137 | 59, 28 | ffvelcdmd 7084 |
. . . . . . . . . . . . . 14
β’ (π β ((1st
βπΉ)βπ) β π) |
138 | 137 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((1st βπΉ)βπ) β π) |
139 | 7, 69, 10, 70, 110 | natcl 17900 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (πβπ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st βπΉ)βπ))) |
140 | 18, 40, 70, 135, 138 | elsetchom 18027 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st βπΉ)βπ)) β (πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ))) |
141 | 139, 140 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ)) |
142 | 10, 118, 70, 56, 28, 27 | funcf2 17814 |
. . . . . . . . . . . . . . . 16
β’ (π β (π(2nd βπΉ)π):(π(Hom βπ)π)βΆ(((1st βπΉ)βπ)(Hom βπ)((1st βπΉ)βπ))) |
143 | 142, 121 | ffvelcdmd 7084 |
. . . . . . . . . . . . . . 15
β’ (π β ((π(2nd βπΉ)π)βπΎ) β (((1st βπΉ)βπ)(Hom βπ)((1st βπΉ)βπ))) |
144 | 18, 22, 70, 137, 60 | elsetchom 18027 |
. . . . . . . . . . . . . . 15
β’ (π β (((π(2nd βπΉ)π)βπΎ) β (((1st βπΉ)βπ)(Hom βπ)((1st βπΉ)βπ)) β ((π(2nd βπΉ)π)βπΎ):((1st βπΉ)βπ)βΆ((1st βπΉ)βπ))) |
145 | 143, 144 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β ((π(2nd βπΉ)π)βπΎ):((1st βπΉ)βπ)βΆ((1st βπΉ)βπ)) |
146 | 145 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((π(2nd βπΉ)π)βπΎ):((1st βπΉ)βπ)βΆ((1st βπΉ)βπ)) |
147 | 18, 40, 11, 135, 138, 61, 141, 146 | setcco 18029 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π(2nd βπΉ)π)βπΎ)(β¨((1st
β((1st βπ)βπ))βπ), ((1st βπΉ)βπ)β©(compβπ)((1st βπΉ)βπ))(πβπ)) = (((π(2nd βπΉ)π)βπΎ) β (πβπ))) |
148 | 134, 136,
147 | 3eqtr3d 2780 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ) β ((π(2nd β((1st
βπ)βπ))π)βπΎ)) = (((π(2nd βπΉ)π)βπΎ) β (πβπ))) |
149 | 148 | fveq1d 6890 |
. . . . . . . . . 10
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((πβπ) β ((π(2nd β((1st
βπ)βπ))π)βπΎ))β( 1 βπ)) = ((((π(2nd βπΉ)π)βπΎ) β (πβπ))β( 1 βπ))) |
150 | 127 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ( 1 βπ) β (π(Hom βπΆ)π)) |
151 | 16, 9, 109, 110, 13, 110, 111, 37, 112, 150 | yon12 18214 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π(2nd β((1st
βπ)βπ))π)βπΎ)β( 1 βπ)) = (( 1 βπ)(β¨π, πβ©(compβπΆ)π)πΎ)) |
152 | 9, 13, 99, 109, 37, 111, 110, 112 | catlid 17623 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (( 1 βπ)(β¨π, πβ©(compβπΆ)π)πΎ) = πΎ) |
153 | 151, 152 | eqtrd 2772 |
. . . . . . . . . . 11
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π(2nd β((1st
βπ)βπ))π)βπΎ)β( 1 βπ)) = πΎ) |
154 | 153 | fveq2d 6892 |
. . . . . . . . . 10
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ)β(((π(2nd β((1st
βπ)βπ))π)βπΎ)β( 1 βπ))) = ((πβπ)βπΎ)) |
155 | 132, 149,
154 | 3eqtr3d 2780 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((((π(2nd βπΉ)π)βπΎ) β (πβπ))β( 1 βπ)) = ((πβπ)βπΎ)) |
156 | | fvco3 6987 |
. . . . . . . . . 10
β’ (((πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ) β§ ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) β ((((π(2nd βπΉ)π)βπΎ) β (πβπ))β( 1 βπ)) = (((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ)))) |
157 | 141, 130,
156 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((((π(2nd βπΉ)π)βπΎ) β (πβπ))β( 1 βπ)) = (((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ)))) |
158 | 117, 155,
157 | 3eqtr2d 2778 |
. . . . . . . 8
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ)β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ))) = (((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ)))) |
159 | 158 | fveq2d 6892 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((π΄βπ)β((πβπ)β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ)))) = ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ))))) |
160 | 108, 159 | eqtrd 2772 |
. . . . . 6
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (((π΄βπ) β (πβπ))β((((π(2nd βπ)π)βπΎ)βπ)β( 1 βπ))) = ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ))))) |
161 | 98, 105, 160 | 3eqtrd 2776 |
. . . . 5
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ)) = ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ))))) |
162 | 161 | mpteq2dva 5247 |
. . . 4
β’ (π β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ))) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ)))))) |
163 | 5, 162 | eqtrid 2784 |
. . 3
β’ (π β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ))) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ)))))) |
164 | | eqid 2732 |
. . . . . . . . . . 11
β’ (π Γc
π) = (π Γc π) |
165 | 164, 43, 10 | xpcbas 18126 |
. . . . . . . . . 10
β’ ((π Func π) Γ π΅) = (Baseβ(π Γc π)) |
166 | | eqid 2732 |
. . . . . . . . . 10
β’ (Hom
β(π
Γc π)) = (Hom β(π Γc π)) |
167 | | eqid 2732 |
. . . . . . . . . 10
β’ (Hom
βπ) = (Hom
βπ) |
168 | | relfunc 17808 |
. . . . . . . . . . 11
β’ Rel
((π
Γc π) Func π) |
169 | | yoneda.t |
. . . . . . . . . . . . 13
β’ π = (SetCatβπ) |
170 | | yoneda.h |
. . . . . . . . . . . . 13
β’ π» =
(HomFβπ) |
171 | | yoneda.r |
. . . . . . . . . . . . 13
β’ π
= ((π Γc π) FuncCat π) |
172 | | yoneda.e |
. . . . . . . . . . . . 13
β’ πΈ = (π evalF π) |
173 | | yoneda.z |
. . . . . . . . . . . . 13
β’ π = (π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))) |
174 | 16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20 | yonedalem1 18221 |
. . . . . . . . . . . 12
β’ (π β (π β ((π Γc π) Func π) β§ πΈ β ((π Γc π) Func π))) |
175 | 174 | simpld 495 |
. . . . . . . . . . 11
β’ (π β π β ((π Γc π) Func π)) |
176 | | 1st2ndbr 8024 |
. . . . . . . . . . 11
β’ ((Rel
((π
Γc π) Func π) β§ π β ((π Γc π) Func π)) β (1st βπ)((π Γc π) Func π)(2nd βπ)) |
177 | 168, 175,
176 | sylancr 587 |
. . . . . . . . . 10
β’ (π β (1st
βπ)((π Γc
π) Func π)(2nd βπ)) |
178 | 54, 28 | opelxpd 5713 |
. . . . . . . . . 10
β’ (π β β¨πΉ, πβ© β ((π Func π) Γ π΅)) |
179 | 62, 27 | opelxpd 5713 |
. . . . . . . . . 10
β’ (π β β¨πΊ, πβ© β ((π Func π) Γ π΅)) |
180 | 165, 166,
167, 177, 178, 179 | funcf2 17814 |
. . . . . . . . 9
β’ (π β (β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©):(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©)βΆ(((1st
βπ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπ)ββ¨πΊ, πβ©))) |
181 | 164, 43, 10, 14, 118, 54, 28, 62, 27, 166 | xpchom2 18134 |
. . . . . . . . . . 11
β’ (π β (β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©) = ((πΉ(π Nat π)πΊ) Γ (π(Hom βπ)π))) |
182 | 120 | xpeq2i 5702 |
. . . . . . . . . . 11
β’ ((πΉ(π Nat π)πΊ) Γ (π(Hom βπ)π)) = ((πΉ(π Nat π)πΊ) Γ (π(Hom βπΆ)π)) |
183 | 181, 182 | eqtrdi 2788 |
. . . . . . . . . 10
β’ (π β (β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©) = ((πΉ(π Nat π)πΊ) Γ (π(Hom βπΆ)π))) |
184 | | df-ov 7408 |
. . . . . . . . . . . . 13
β’ (πΉ(1st βπ)π) = ((1st βπ)ββ¨πΉ, πβ©) |
185 | | df-ov 7408 |
. . . . . . . . . . . . 13
β’ (πΊ(1st βπ)π) = ((1st βπ)ββ¨πΊ, πβ©) |
186 | 184, 185 | oveq12i 7417 |
. . . . . . . . . . . 12
β’ ((πΉ(1st βπ)π)(Hom βπ)(πΊ(1st βπ)π)) = (((1st βπ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπ)ββ¨πΊ, πβ©)) |
187 | 186 | eqcomi 2741 |
. . . . . . . . . . 11
β’
(((1st βπ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπ)ββ¨πΊ, πβ©)) = ((πΉ(1st βπ)π)(Hom βπ)(πΊ(1st βπ)π)) |
188 | 187 | a1i 11 |
. . . . . . . . . 10
β’ (π β (((1st
βπ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπ)ββ¨πΊ, πβ©)) = ((πΉ(1st βπ)π)(Hom βπ)(πΊ(1st βπ)π))) |
189 | 183, 188 | feq23d 6709 |
. . . . . . . . 9
β’ (π β ((β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©):(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©)βΆ(((1st
βπ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπ)ββ¨πΊ, πβ©)) β (β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©):((πΉ(π Nat π)πΊ) Γ (π(Hom βπΆ)π))βΆ((πΉ(1st βπ)π)(Hom βπ)(πΊ(1st βπ)π)))) |
190 | 180, 189 | mpbid 231 |
. . . . . . . 8
β’ (π β (β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©):((πΉ(π Nat π)πΊ) Γ (π(Hom βπΆ)π))βΆ((πΉ(1st βπ)π)(Hom βπ)(πΊ(1st βπ)π))) |
191 | 190, 34, 30 | fovcdmd 7575 |
. . . . . . 7
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) β ((πΉ(1st βπ)π)(Hom βπ)(πΊ(1st βπ)π))) |
192 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
193 | 165, 192,
177 | funcf1 17812 |
. . . . . . . . . 10
β’ (π β (1st
βπ):((π Func π) Γ π΅)βΆ(Baseβπ)) |
194 | 193, 54, 28 | fovcdmd 7575 |
. . . . . . . . 9
β’ (π β (πΉ(1st βπ)π) β (Baseβπ)) |
195 | 169, 19 | setcbas 18024 |
. . . . . . . . 9
β’ (π β π = (Baseβπ)) |
196 | 194, 195 | eleqtrrd 2836 |
. . . . . . . 8
β’ (π β (πΉ(1st βπ)π) β π) |
197 | 193, 62, 27 | fovcdmd 7575 |
. . . . . . . . 9
β’ (π β (πΊ(1st βπ)π) β (Baseβπ)) |
198 | 197, 195 | eleqtrrd 2836 |
. . . . . . . 8
β’ (π β (πΊ(1st βπ)π) β π) |
199 | 169, 19, 167, 196, 198 | elsetchom 18027 |
. . . . . . 7
β’ (π β ((π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) β ((πΉ(1st βπ)π)(Hom βπ)(πΊ(1st βπ)π)) β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ):(πΉ(1st βπ)π)βΆ(πΊ(1st βπ)π))) |
200 | 191, 199 | mpbid 231 |
. . . . . 6
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ):(πΉ(1st βπ)π)βΆ(πΊ(1st βπ)π)) |
201 | 16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 62, 27, 34, 30 | yonedalem22 18227 |
. . . . . . . 8
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) = (((π(2nd βπ)π)βπΎ)(β¨((1st βπ)βπ), πΉβ©(2nd βπ»)β¨((1st
βπ)βπ), πΊβ©)π΄)) |
202 | 8 | oppccat 17664 |
. . . . . . . . . . 11
β’ (πΆ β Cat β π β Cat) |
203 | 17, 202 | syl 17 |
. . . . . . . . . 10
β’ (π β π β Cat) |
204 | 18 | setccat 18031 |
. . . . . . . . . . 11
β’ (π β V β π β Cat) |
205 | 22, 204 | syl 17 |
. . . . . . . . . 10
β’ (π β π β Cat) |
206 | 6, 203, 205 | fuccat 17919 |
. . . . . . . . 9
β’ (π β π β Cat) |
207 | 170, 206,
43, 14, 45, 54, 82, 62, 12, 31, 34 | hof2val 18205 |
. . . . . . . 8
β’ (π β (((π(2nd βπ)π)βπΎ)(β¨((1st βπ)βπ), πΉβ©(2nd βπ»)β¨((1st
βπ)βπ), πΊβ©)π΄) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ)))) |
208 | 201, 207 | eqtrd 2772 |
. . . . . . 7
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ)))) |
209 | 16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28 | yonedalem21 18222 |
. . . . . . 7
β’ (π β (πΉ(1st βπ)π) = (((1st βπ)βπ)(π Nat π)πΉ)) |
210 | 16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27 | yonedalem21 18222 |
. . . . . . 7
β’ (π β (πΊ(1st βπ)π) = (((1st βπ)βπ)(π Nat π)πΊ)) |
211 | 208, 209,
210 | feq123d 6703 |
. . . . . 6
β’ (π β ((π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ):(πΉ(1st βπ)π)βΆ(πΊ(1st βπ)π) β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))):(((1st βπ)βπ)(π Nat π)πΉ)βΆ(((1st βπ)βπ)(π Nat π)πΊ))) |
212 | 200, 211 | mpbid 231 |
. . . . 5
β’ (π β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))):(((1st βπ)βπ)(π Nat π)πΉ)βΆ(((1st βπ)βπ)(π Nat π)πΊ)) |
213 | | eqid 2732 |
. . . . . 6
β’ (π β (((1st
βπ)βπ)(π Nat π)πΉ) β¦ ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))) |
214 | 213 | fmpt 7106 |
. . . . 5
β’
(βπ β
(((1st βπ)βπ)(π Nat π)πΉ)((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ)) β (((1st βπ)βπ)(π Nat π)πΊ) β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))):(((1st βπ)βπ)(π Nat π)πΉ)βΆ(((1st βπ)βπ)(π Nat π)πΊ)) |
215 | 212, 214 | sylibr 233 |
. . . 4
β’ (π β βπ β (((1st βπ)βπ)(π Nat π)πΉ)((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ)) β (((1st βπ)βπ)(π Nat π)πΊ)) |
216 | | yonedalem3.m |
. . . . . 6
β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) |
217 | 16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27, 216 | yonedalem3a 18223 |
. . . . 5
β’ (π β ((πΊππ) = (π β (((1st βπ)βπ)(π Nat π)πΊ) β¦ ((πβπ)β( 1 βπ))) β§ (πΊππ):(πΊ(1st βπ)π)βΆ(πΊ(1st βπΈ)π))) |
218 | 217 | simpld 495 |
. . . 4
β’ (π β (πΊππ) = (π β (((1st βπ)βπ)(π Nat π)πΊ) β¦ ((πβπ)β( 1 βπ)))) |
219 | | fveq1 6887 |
. . . . 5
β’ (π = ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ)) β (πβπ) = (((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)) |
220 | 219 | fveq1d 6890 |
. . . 4
β’ (π = ((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ)) β ((πβπ)β( 1 βπ)) = ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ))) |
221 | 215, 208,
218, 220 | fmptcof 7124 |
. . 3
β’ (π β ((πΊππ) β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ)) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((((π΄(β¨((1st βπ)βπ), πΉβ©(compβπ)πΊ)π)(β¨((1st βπ)βπ), ((1st βπ)βπ)β©(compβπ)πΊ)((π(2nd βπ)π)βπΎ))βπ)β( 1 βπ)))) |
222 | | eqid 2732 |
. . . . . . 7
β’
(β¨πΉ, πβ©(2nd
βπΈ)β¨πΊ, πβ©) = (β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©) |
223 | 172, 203,
205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121 | evlf2val 18168 |
. . . . . 6
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ) = ((π΄βπ)(β¨((1st βπΉ)βπ), ((1st βπΉ)βπ)β©(compβπ)((1st βπΊ)βπ))((π(2nd βπΉ)π)βπΎ))) |
224 | 18, 22, 11, 137, 60, 67, 145, 77 | setcco 18029 |
. . . . . 6
β’ (π β ((π΄βπ)(β¨((1st βπΉ)βπ), ((1st βπΉ)βπ)β©(compβπ)((1st βπΊ)βπ))((π(2nd βπΉ)π)βπΎ)) = ((π΄βπ) β ((π(2nd βπΉ)π)βπΎ))) |
225 | 223, 224 | eqtrd 2772 |
. . . . 5
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ) = ((π΄βπ) β ((π(2nd βπΉ)π)βπΎ))) |
226 | 225 | coeq1d 5859 |
. . . 4
β’ (π β ((π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ) β (πΉππ)) = (((π΄βπ) β ((π(2nd βπΉ)π)βπΎ)) β (πΉππ))) |
227 | 16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 216 | yonedalem3a 18223 |
. . . . . . . 8
β’ (π β ((πΉππ) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))) β§ (πΉππ):(πΉ(1st βπ)π)βΆ(πΉ(1st βπΈ)π))) |
228 | 227 | simprd 496 |
. . . . . . 7
β’ (π β (πΉππ):(πΉ(1st βπ)π)βΆ(πΉ(1st βπΈ)π)) |
229 | 227 | simpld 495 |
. . . . . . . 8
β’ (π β (πΉππ) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ)))) |
230 | 172, 203,
205, 10, 54, 28 | evlf1 18169 |
. . . . . . . 8
β’ (π β (πΉ(1st βπΈ)π) = ((1st βπΉ)βπ)) |
231 | 229, 209,
230 | feq123d 6703 |
. . . . . . 7
β’ (π β ((πΉππ):(πΉ(1st βπ)π)βΆ(πΉ(1st βπΈ)π) β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))):(((1st βπ)βπ)(π Nat π)πΉ)βΆ((1st βπΉ)βπ))) |
232 | 228, 231 | mpbid 231 |
. . . . . 6
β’ (π β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))):(((1st βπ)βπ)(π Nat π)πΉ)βΆ((1st βπΉ)βπ)) |
233 | | eqid 2732 |
. . . . . . 7
β’ (π β (((1st
βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))) |
234 | 233 | fmpt 7106 |
. . . . . 6
β’
(βπ β
(((1st βπ)βπ)(π Nat π)πΉ)((πβπ)β( 1 βπ)) β ((1st βπΉ)βπ) β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))):(((1st βπ)βπ)(π Nat π)πΉ)βΆ((1st βπΉ)βπ)) |
235 | 232, 234 | sylibr 233 |
. . . . 5
β’ (π β βπ β (((1st βπ)βπ)(π Nat π)πΉ)((πβπ)β( 1 βπ)) β ((1st βπΉ)βπ)) |
236 | | fcompt 7127 |
. . . . . 6
β’ (((π΄βπ):((1st βπΉ)βπ)βΆ((1st βπΊ)βπ) β§ ((π(2nd βπΉ)π)βπΎ):((1st βπΉ)βπ)βΆ((1st βπΉ)βπ)) β ((π΄βπ) β ((π(2nd βπΉ)π)βπΎ)) = (π¦ β ((1st βπΉ)βπ) β¦ ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)βπ¦)))) |
237 | 77, 145, 236 | syl2anc 584 |
. . . . 5
β’ (π β ((π΄βπ) β ((π(2nd βπΉ)π)βπΎ)) = (π¦ β ((1st βπΉ)βπ) β¦ ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)βπ¦)))) |
238 | | 2fveq3 6893 |
. . . . 5
β’ (π¦ = ((πβπ)β( 1 βπ)) β ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)βπ¦)) = ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ))))) |
239 | 235, 229,
237, 238 | fmptcof 7124 |
. . . 4
β’ (π β (((π΄βπ) β ((π(2nd βπΉ)π)βπΎ)) β (πΉππ)) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ)))))) |
240 | 226, 239 | eqtrd 2772 |
. . 3
β’ (π β ((π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ) β (πΉππ)) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((π΄βπ)β(((π(2nd βπΉ)π)βπΎ)β((πβπ)β( 1 βπ)))))) |
241 | 163, 221,
240 | 3eqtr4d 2782 |
. 2
β’ (π β ((πΊππ) β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ)) = ((π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ) β (πΉππ))) |
242 | | eqid 2732 |
. . 3
β’
(compβπ) =
(compβπ) |
243 | 174 | simprd 496 |
. . . . . . 7
β’ (π β πΈ β ((π Γc π) Func π)) |
244 | | 1st2ndbr 8024 |
. . . . . . 7
β’ ((Rel
((π
Γc π) Func π) β§ πΈ β ((π Γc π) Func π)) β (1st βπΈ)((π Γc π) Func π)(2nd βπΈ)) |
245 | 168, 243,
244 | sylancr 587 |
. . . . . 6
β’ (π β (1st
βπΈ)((π Γc
π) Func π)(2nd βπΈ)) |
246 | 165, 192,
245 | funcf1 17812 |
. . . . 5
β’ (π β (1st
βπΈ):((π Func π) Γ π΅)βΆ(Baseβπ)) |
247 | 246, 62, 27 | fovcdmd 7575 |
. . . 4
β’ (π β (πΊ(1st βπΈ)π) β (Baseβπ)) |
248 | 247, 195 | eleqtrrd 2836 |
. . 3
β’ (π β (πΊ(1st βπΈ)π) β π) |
249 | 217 | simprd 496 |
. . 3
β’ (π β (πΊππ):(πΊ(1st βπ)π)βΆ(πΊ(1st βπΈ)π)) |
250 | 169, 19, 242, 196, 198, 248, 200, 249 | setcco 18029 |
. 2
β’ (π β ((πΊππ)(β¨(πΉ(1st βπ)π), (πΊ(1st βπ)π)β©(compβπ)(πΊ(1st βπΈ)π))(π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ)) = ((πΊππ) β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ))) |
251 | 246, 54, 28 | fovcdmd 7575 |
. . . 4
β’ (π β (πΉ(1st βπΈ)π) β (Baseβπ)) |
252 | 251, 195 | eleqtrrd 2836 |
. . 3
β’ (π β (πΉ(1st βπΈ)π) β π) |
253 | 165, 166,
167, 245, 178, 179 | funcf2 17814 |
. . . . . 6
β’ (π β (β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©):(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©)βΆ(((1st
βπΈ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπΈ)ββ¨πΊ, πβ©))) |
254 | | df-ov 7408 |
. . . . . . . . . 10
β’ (πΉ(1st βπΈ)π) = ((1st βπΈ)ββ¨πΉ, πβ©) |
255 | | df-ov 7408 |
. . . . . . . . . 10
β’ (πΊ(1st βπΈ)π) = ((1st βπΈ)ββ¨πΊ, πβ©) |
256 | 254, 255 | oveq12i 7417 |
. . . . . . . . 9
β’ ((πΉ(1st βπΈ)π)(Hom βπ)(πΊ(1st βπΈ)π)) = (((1st βπΈ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπΈ)ββ¨πΊ, πβ©)) |
257 | 256 | eqcomi 2741 |
. . . . . . . 8
β’
(((1st βπΈ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπΈ)ββ¨πΊ, πβ©)) = ((πΉ(1st βπΈ)π)(Hom βπ)(πΊ(1st βπΈ)π)) |
258 | 257 | a1i 11 |
. . . . . . 7
β’ (π β (((1st
βπΈ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπΈ)ββ¨πΊ, πβ©)) = ((πΉ(1st βπΈ)π)(Hom βπ)(πΊ(1st βπΈ)π))) |
259 | 183, 258 | feq23d 6709 |
. . . . . 6
β’ (π β ((β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©):(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©)βΆ(((1st
βπΈ)ββ¨πΉ, πβ©)(Hom βπ)((1st βπΈ)ββ¨πΊ, πβ©)) β (β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©):((πΉ(π Nat π)πΊ) Γ (π(Hom βπΆ)π))βΆ((πΉ(1st βπΈ)π)(Hom βπ)(πΊ(1st βπΈ)π)))) |
260 | 253, 259 | mpbid 231 |
. . . . 5
β’ (π β (β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©):((πΉ(π Nat π)πΊ) Γ (π(Hom βπΆ)π))βΆ((πΉ(1st βπΈ)π)(Hom βπ)(πΊ(1st βπΈ)π))) |
261 | 260, 34, 30 | fovcdmd 7575 |
. . . 4
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ) β ((πΉ(1st βπΈ)π)(Hom βπ)(πΊ(1st βπΈ)π))) |
262 | 169, 19, 167, 252, 248 | elsetchom 18027 |
. . . 4
β’ (π β ((π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ) β ((πΉ(1st βπΈ)π)(Hom βπ)(πΊ(1st βπΈ)π)) β (π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ):(πΉ(1st βπΈ)π)βΆ(πΊ(1st βπΈ)π))) |
263 | 261, 262 | mpbid 231 |
. . 3
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ):(πΉ(1st βπΈ)π)βΆ(πΊ(1st βπΈ)π)) |
264 | 169, 19, 242, 196, 252, 248, 228, 263 | setcco 18029 |
. 2
β’ (π β ((π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ)(β¨(πΉ(1st βπ)π), (πΉ(1st βπΈ)π)β©(compβπ)(πΊ(1st βπΈ)π))(πΉππ)) = ((π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ) β (πΉππ))) |
265 | 241, 250,
264 | 3eqtr4d 2782 |
1
β’ (π β ((πΊππ)(β¨(πΉ(1st βπ)π), (πΊ(1st βπ)π)β©(compβπ)(πΊ(1st βπΈ)π))(π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ)) = ((π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ)(β¨(πΉ(1st βπ)π), (πΉ(1st βπΈ)π)β©(compβπ)(πΊ(1st βπΈ)π))(πΉππ))) |