Step | Hyp | Ref
| Expression |
1 | | yoneda.y |
. . . . 5
β’ π = (YonβπΆ) |
2 | | yoneda.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
3 | | yoneda.1 |
. . . . 5
β’ 1 =
(IdβπΆ) |
4 | | yoneda.o |
. . . . 5
β’ π = (oppCatβπΆ) |
5 | | yoneda.s |
. . . . 5
β’ π = (SetCatβπ) |
6 | | yoneda.t |
. . . . 5
β’ π = (SetCatβπ) |
7 | | yoneda.q |
. . . . 5
β’ π = (π FuncCat π) |
8 | | yoneda.h |
. . . . 5
β’ π» =
(HomFβπ) |
9 | | yoneda.r |
. . . . 5
β’ π
= ((π Γc π) FuncCat π) |
10 | | yoneda.e |
. . . . 5
β’ πΈ = (π evalF π) |
11 | | yoneda.z |
. . . . 5
β’ π = (π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))) |
12 | | yoneda.c |
. . . . 5
β’ (π β πΆ β Cat) |
13 | | yoneda.w |
. . . . 5
β’ (π β π β π) |
14 | | yoneda.u |
. . . . 5
β’ (π β ran
(Homf βπΆ) β π) |
15 | | yoneda.v |
. . . . 5
β’ (π β (ran
(Homf βπ) βͺ π) β π) |
16 | | yonedalem21.f |
. . . . 5
β’ (π β πΉ β (π Func π)) |
17 | | yonedalem21.x |
. . . . 5
β’ (π β π β π΅) |
18 | | yonedalem4.n |
. . . . 5
β’ π = (π β (π Func π), π₯ β π΅ β¦ (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’))))) |
19 | | yonedalem4.p |
. . . . 5
β’ (π β π΄ β ((1st βπΉ)βπ)) |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19 | yonedalem4a 18212 |
. . . 4
β’ (π β ((πΉππ)βπ΄) = (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))) |
21 | 20 | fveq1d 6881 |
. . 3
β’ (π β (((πΉππ)βπ΄)βπ) = ((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ)) |
22 | 21 | fveq1d 6881 |
. 2
β’ (π β ((((πΉππ)βπ΄)βπ)βπΊ) = (((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ)βπΊ)) |
23 | | eqidd 2733 |
. . 3
β’ (π β (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄))) = (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))) |
24 | | yonedalem4b.p |
. . . 4
β’ (π β π β π΅) |
25 | | ovex 7427 |
. . . . . 6
β’ (π¦(Hom βπΆ)π) β V |
26 | 25 | mptex 7210 |
. . . . 5
β’ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)) β V |
27 | 26 | a1i 11 |
. . . 4
β’ ((π β§ π¦ = π) β (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)) β V) |
28 | | yonedalem4b.g |
. . . . . . 7
β’ (π β πΊ β (π(Hom βπΆ)π)) |
29 | 28 | adantr 481 |
. . . . . 6
β’ ((π β§ π¦ = π) β πΊ β (π(Hom βπΆ)π)) |
30 | | simpr 485 |
. . . . . . 7
β’ ((π β§ π¦ = π) β π¦ = π) |
31 | 30 | oveq1d 7409 |
. . . . . 6
β’ ((π β§ π¦ = π) β (π¦(Hom βπΆ)π) = (π(Hom βπΆ)π)) |
32 | 29, 31 | eleqtrrd 2836 |
. . . . 5
β’ ((π β§ π¦ = π) β πΊ β (π¦(Hom βπΆ)π)) |
33 | | fvexd 6894 |
. . . . 5
β’ (((π β§ π¦ = π) β§ π = πΊ) β (((π(2nd βπΉ)π¦)βπ)βπ΄) β V) |
34 | | simplr 767 |
. . . . . . . 8
β’ (((π β§ π¦ = π) β§ π = πΊ) β π¦ = π) |
35 | 34 | oveq2d 7410 |
. . . . . . 7
β’ (((π β§ π¦ = π) β§ π = πΊ) β (π(2nd βπΉ)π¦) = (π(2nd βπΉ)π)) |
36 | | simpr 485 |
. . . . . . 7
β’ (((π β§ π¦ = π) β§ π = πΊ) β π = πΊ) |
37 | 35, 36 | fveq12d 6886 |
. . . . . 6
β’ (((π β§ π¦ = π) β§ π = πΊ) β ((π(2nd βπΉ)π¦)βπ) = ((π(2nd βπΉ)π)βπΊ)) |
38 | 37 | fveq1d 6881 |
. . . . 5
β’ (((π β§ π¦ = π) β§ π = πΊ) β (((π(2nd βπΉ)π¦)βπ)βπ΄) = (((π(2nd βπΉ)π)βπΊ)βπ΄)) |
39 | 32, 33, 38 | fvmptdv2 7003 |
. . . 4
β’ ((π β§ π¦ = π) β (((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ) = (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)) β (((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ)βπΊ) = (((π(2nd βπΉ)π)βπΊ)βπ΄))) |
40 | | nfmpt1 5250 |
. . . 4
β’
β²π¦(π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄))) |
41 | | nffvmpt1 6890 |
. . . . . 6
β’
β²π¦((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ) |
42 | | nfcv 2903 |
. . . . . 6
β’
β²π¦πΊ |
43 | 41, 42 | nffv 6889 |
. . . . 5
β’
β²π¦(((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ)βπΊ) |
44 | 43 | nfeq1 2918 |
. . . 4
β’
β²π¦(((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ)βπΊ) = (((π(2nd βπΉ)π)βπΊ)βπ΄) |
45 | 24, 27, 39, 40, 44 | fvmptd2f 7001 |
. . 3
β’ (π β ((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄))) = (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄))) β (((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ)βπΊ) = (((π(2nd βπΉ)π)βπΊ)βπ΄))) |
46 | 23, 45 | mpd 15 |
. 2
β’ (π β (((π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))βπ)βπΊ) = (((π(2nd βπΉ)π)βπΊ)βπ΄)) |
47 | 22, 46 | eqtrd 2772 |
1
β’ (π β ((((πΉππ)βπ΄)βπ)βπΊ) = (((π(2nd βπΉ)π)βπΊ)βπ΄)) |