Step | Hyp | Ref
| Expression |
1 | | yonedalem4.n |
. . . 4
β’ π = (π β (π Func π), π₯ β π΅ β¦ (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’))))) |
2 | 1 | a1i 11 |
. . 3
β’ (π β π = (π β (π Func π), π₯ β π΅ β¦ (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’)))))) |
3 | | simprl 769 |
. . . . . 6
β’ ((π β§ (π = πΉ β§ π₯ = π)) β π = πΉ) |
4 | 3 | fveq2d 6808 |
. . . . 5
β’ ((π β§ (π = πΉ β§ π₯ = π)) β (1st βπ) = (1st βπΉ)) |
5 | | simprr 771 |
. . . . 5
β’ ((π β§ (π = πΉ β§ π₯ = π)) β π₯ = π) |
6 | 4, 5 | fveq12d 6811 |
. . . 4
β’ ((π β§ (π = πΉ β§ π₯ = π)) β ((1st βπ)βπ₯) = ((1st βπΉ)βπ)) |
7 | | simplrr 776 |
. . . . . . 7
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β π₯ = π) |
8 | 7 | oveq2d 7323 |
. . . . . 6
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β (π¦(Hom βπΆ)π₯) = (π¦(Hom βπΆ)π)) |
9 | | simplrl 775 |
. . . . . . . . . 10
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β π = πΉ) |
10 | 9 | fveq2d 6808 |
. . . . . . . . 9
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β (2nd βπ) = (2nd βπΉ)) |
11 | | eqidd 2737 |
. . . . . . . . 9
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β π¦ = π¦) |
12 | 10, 7, 11 | oveq123d 7328 |
. . . . . . . 8
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β (π₯(2nd βπ)π¦) = (π(2nd βπΉ)π¦)) |
13 | 12 | fveq1d 6806 |
. . . . . . 7
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β ((π₯(2nd βπ)π¦)βπ) = ((π(2nd βπΉ)π¦)βπ)) |
14 | 13 | fveq1d 6806 |
. . . . . 6
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β (((π₯(2nd βπ)π¦)βπ)βπ’) = (((π(2nd βπΉ)π¦)βπ)βπ’)) |
15 | 8, 14 | mpteq12dv 5172 |
. . . . 5
β’ (((π β§ (π = πΉ β§ π₯ = π)) β§ π¦ β π΅) β (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’)) = (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ’))) |
16 | 15 | mpteq2dva 5181 |
. . . 4
β’ ((π β§ (π = πΉ β§ π₯ = π)) β (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’))) = (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ’)))) |
17 | 6, 16 | mpteq12dv 5172 |
. . 3
β’ ((π β§ (π = πΉ β§ π₯ = π)) β (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’)))) = (π’ β ((1st βπΉ)βπ) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ’))))) |
18 | | yonedalem21.f |
. . 3
β’ (π β πΉ β (π Func π)) |
19 | | yonedalem21.x |
. . 3
β’ (π β π β π΅) |
20 | | fvex 6817 |
. . . . 5
β’
((1st βπΉ)βπ) β V |
21 | 20 | mptex 7131 |
. . . 4
β’ (π’ β ((1st
βπΉ)βπ) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ’)))) β V |
22 | 21 | a1i 11 |
. . 3
β’ (π β (π’ β ((1st βπΉ)βπ) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ’)))) β V) |
23 | 2, 17, 18, 19, 22 | ovmpod 7457 |
. 2
β’ (π β (πΉππ) = (π’ β ((1st βπΉ)βπ) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ’))))) |
24 | | simpr 486 |
. . . . 5
β’ ((π β§ π’ = π΄) β π’ = π΄) |
25 | 24 | fveq2d 6808 |
. . . 4
β’ ((π β§ π’ = π΄) β (((π(2nd βπΉ)π¦)βπ)βπ’) = (((π(2nd βπΉ)π¦)βπ)βπ΄)) |
26 | 25 | mpteq2dv 5183 |
. . 3
β’ ((π β§ π’ = π΄) β (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ’)) = (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄))) |
27 | 26 | mpteq2dv 5183 |
. 2
β’ ((π β§ π’ = π΄) β (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ’))) = (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))) |
28 | | yonedalem4.p |
. 2
β’ (π β π΄ β ((1st βπΉ)βπ)) |
29 | | yoneda.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
30 | 29 | fvexi 6818 |
. . . 4
β’ π΅ β V |
31 | 30 | mptex 7131 |
. . 3
β’ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄))) β V |
32 | 31 | a1i 11 |
. 2
β’ (π β (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄))) β V) |
33 | 23, 27, 28, 32 | fvmptd 6914 |
1
β’ (π β ((πΉππ)βπ΄) = (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))) |