Step | Hyp | Ref
| Expression |
1 | | yonedalem21.f |
. . 3
β’ (π β πΉ β (π Func π)) |
2 | | yonedalem21.x |
. . 3
β’ (π β π β π΅) |
3 | | simpr 486 |
. . . . . . 7
β’ ((π = πΉ β§ π₯ = π) β π₯ = π) |
4 | 3 | fveq2d 6847 |
. . . . . 6
β’ ((π = πΉ β§ π₯ = π) β ((1st βπ)βπ₯) = ((1st βπ)βπ)) |
5 | | simpl 484 |
. . . . . 6
β’ ((π = πΉ β§ π₯ = π) β π = πΉ) |
6 | 4, 5 | oveq12d 7376 |
. . . . 5
β’ ((π = πΉ β§ π₯ = π) β (((1st βπ)βπ₯)(π Nat π)π) = (((1st βπ)βπ)(π Nat π)πΉ)) |
7 | 3 | fveq2d 6847 |
. . . . . 6
β’ ((π = πΉ β§ π₯ = π) β (πβπ₯) = (πβπ)) |
8 | 3 | fveq2d 6847 |
. . . . . 6
β’ ((π = πΉ β§ π₯ = π) β ( 1 βπ₯) = ( 1 βπ)) |
9 | 7, 8 | fveq12d 6850 |
. . . . 5
β’ ((π = πΉ β§ π₯ = π) β ((πβπ₯)β( 1 βπ₯)) = ((πβπ)β( 1 βπ))) |
10 | 6, 9 | mpteq12dv 5197 |
. . . 4
β’ ((π = πΉ β§ π₯ = π) β (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯))) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ)))) |
11 | | yonedalem3a.m |
. . . 4
β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) |
12 | | ovex 7391 |
. . . . 5
β’
(((1st βπ)βπ)(π Nat π)πΉ) β V |
13 | 12 | mptex 7174 |
. . . 4
β’ (π β (((1st
βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))) β V |
14 | 10, 11, 13 | ovmpoa 7511 |
. . 3
β’ ((πΉ β (π Func π) β§ π β π΅) β (πΉππ) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ)))) |
15 | 1, 2, 14 | syl2anc 585 |
. 2
β’ (π β (πΉππ) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ)))) |
16 | | eqid 2733 |
. . . . . . 7
β’ (π Nat π) = (π Nat π) |
17 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β (((1st βπ)βπ)(π Nat π)πΉ)) |
18 | 16, 17 | nat1st2nd 17843 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β (β¨(1st
β((1st βπ)βπ)), (2nd β((1st
βπ)βπ))β©(π Nat π)β¨(1st βπΉ), (2nd βπΉ)β©)) |
19 | | yoneda.o |
. . . . . . . 8
β’ π = (oppCatβπΆ) |
20 | | yoneda.b |
. . . . . . . 8
β’ π΅ = (BaseβπΆ) |
21 | 19, 20 | oppcbas 17604 |
. . . . . . 7
β’ π΅ = (Baseβπ) |
22 | | eqid 2733 |
. . . . . . 7
β’ (Hom
βπ) = (Hom
βπ) |
23 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β π΅) |
24 | 16, 18, 21, 22, 23 | natcl 17845 |
. . . . . 6
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (πβπ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st βπΉ)βπ))) |
25 | | yoneda.s |
. . . . . . 7
β’ π = (SetCatβπ) |
26 | | yoneda.w |
. . . . . . . . 9
β’ (π β π β π) |
27 | | yoneda.v |
. . . . . . . . . 10
β’ (π β (ran
(Homf βπ) βͺ π) β π) |
28 | 27 | unssbd 4149 |
. . . . . . . . 9
β’ (π β π β π) |
29 | 26, 28 | ssexd 5282 |
. . . . . . . 8
β’ (π β π β V) |
30 | 29 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β π β V) |
31 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
32 | | relfunc 17753 |
. . . . . . . . . . . 12
β’ Rel
(π Func π) |
33 | | yoneda.y |
. . . . . . . . . . . . 13
β’ π = (YonβπΆ) |
34 | | yoneda.c |
. . . . . . . . . . . . 13
β’ (π β πΆ β Cat) |
35 | | yoneda.u |
. . . . . . . . . . . . 13
β’ (π β ran
(Homf βπΆ) β π) |
36 | 33, 20, 34, 2, 19, 25, 29, 35 | yon1cl 18157 |
. . . . . . . . . . . 12
β’ (π β ((1st
βπ)βπ) β (π Func π)) |
37 | | 1st2ndbr 7975 |
. . . . . . . . . . . 12
β’ ((Rel
(π Func π) β§ ((1st βπ)βπ) β (π Func π)) β (1st
β((1st βπ)βπ))(π Func π)(2nd β((1st
βπ)βπ))) |
38 | 32, 36, 37 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (1st
β((1st βπ)βπ))(π Func π)(2nd β((1st
βπ)βπ))) |
39 | 21, 31, 38 | funcf1 17757 |
. . . . . . . . . 10
β’ (π β (1st
β((1st βπ)βπ)):π΅βΆ(Baseβπ)) |
40 | 39, 2 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (π β ((1st
β((1st βπ)βπ))βπ) β (Baseβπ)) |
41 | 25, 29 | setcbas 17969 |
. . . . . . . . 9
β’ (π β π = (Baseβπ)) |
42 | 40, 41 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β ((1st
β((1st βπ)βπ))βπ) β π) |
43 | 42 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((1st
β((1st βπ)βπ))βπ) β π) |
44 | | 1st2ndbr 7975 |
. . . . . . . . . . . 12
β’ ((Rel
(π Func π) β§ πΉ β (π Func π)) β (1st βπΉ)(π Func π)(2nd βπΉ)) |
45 | 32, 1, 44 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (1st
βπΉ)(π Func π)(2nd βπΉ)) |
46 | 21, 31, 45 | funcf1 17757 |
. . . . . . . . . 10
β’ (π β (1st
βπΉ):π΅βΆ(Baseβπ)) |
47 | 46, 2 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (π β ((1st
βπΉ)βπ) β (Baseβπ)) |
48 | 47, 41 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β ((1st
βπΉ)βπ) β π) |
49 | 48 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((1st βπΉ)βπ) β π) |
50 | 25, 30, 22, 43, 49 | elsetchom 17972 |
. . . . . 6
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ) β (((1st
β((1st βπ)βπ))βπ)(Hom βπ)((1st βπΉ)βπ)) β (πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ))) |
51 | 24, 50 | mpbid 231 |
. . . . 5
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β (πβπ):((1st β((1st
βπ)βπ))βπ)βΆ((1st βπΉ)βπ)) |
52 | | eqid 2733 |
. . . . . . . 8
β’ (Hom
βπΆ) = (Hom
βπΆ) |
53 | | yoneda.1 |
. . . . . . . 8
β’ 1 =
(IdβπΆ) |
54 | 20, 52, 53, 34, 2 | catidcl 17567 |
. . . . . . 7
β’ (π β ( 1 βπ) β (π(Hom βπΆ)π)) |
55 | 33, 20, 34, 2, 52, 2 | yon11 18158 |
. . . . . . 7
β’ (π β ((1st
β((1st βπ)βπ))βπ) = (π(Hom βπΆ)π)) |
56 | 54, 55 | eleqtrrd 2837 |
. . . . . 6
β’ (π β ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) |
57 | 56 | adantr 482 |
. . . . 5
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ( 1 βπ) β ((1st
β((1st βπ)βπ))βπ)) |
58 | 51, 57 | ffvelcdmd 7037 |
. . . 4
β’ ((π β§ π β (((1st βπ)βπ)(π Nat π)πΉ)) β ((πβπ)β( 1 βπ)) β ((1st βπΉ)βπ)) |
59 | 58 | fmpttd 7064 |
. . 3
β’ (π β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))):(((1st βπ)βπ)(π Nat π)πΉ)βΆ((1st βπΉ)βπ)) |
60 | | yoneda.t |
. . . . 5
β’ π = (SetCatβπ) |
61 | | yoneda.q |
. . . . 5
β’ π = (π FuncCat π) |
62 | | yoneda.h |
. . . . 5
β’ π» =
(HomFβπ) |
63 | | yoneda.r |
. . . . 5
β’ π
= ((π Γc π) FuncCat π) |
64 | | yoneda.e |
. . . . 5
β’ πΈ = (π evalF π) |
65 | | yoneda.z |
. . . . 5
β’ π = (π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))) |
66 | 33, 20, 53, 19, 25, 60, 61, 62, 63, 64, 65, 34, 26, 35, 27, 1, 2 | yonedalem21 18167 |
. . . 4
β’ (π β (πΉ(1st βπ)π) = (((1st βπ)βπ)(π Nat π)πΉ)) |
67 | 19 | oppccat 17609 |
. . . . . 6
β’ (πΆ β Cat β π β Cat) |
68 | 34, 67 | syl 17 |
. . . . 5
β’ (π β π β Cat) |
69 | 25 | setccat 17976 |
. . . . . 6
β’ (π β V β π β Cat) |
70 | 29, 69 | syl 17 |
. . . . 5
β’ (π β π β Cat) |
71 | 64, 68, 70, 21, 1, 2 | evlf1 18114 |
. . . 4
β’ (π β (πΉ(1st βπΈ)π) = ((1st βπΉ)βπ)) |
72 | 15, 66, 71 | feq123d 6658 |
. . 3
β’ (π β ((πΉππ):(πΉ(1st βπ)π)βΆ(πΉ(1st βπΈ)π) β (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))):(((1st βπ)βπ)(π Nat π)πΉ)βΆ((1st βπΉ)βπ))) |
73 | 59, 72 | mpbird 257 |
. 2
β’ (π β (πΉππ):(πΉ(1st βπ)π)βΆ(πΉ(1st βπΈ)π)) |
74 | 15, 73 | jca 513 |
1
β’ (π β ((πΉππ) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))) β§ (πΉππ):(πΉ(1st βπ)π)βΆ(πΉ(1st βπΈ)π))) |