Step | Hyp | Ref
| Expression |
1 | | yon11.y |
. . . . . . . . . 10
β’ π = (YonβπΆ) |
2 | | yon11.c |
. . . . . . . . . 10
β’ (π β πΆ β Cat) |
3 | | eqid 2733 |
. . . . . . . . . 10
β’
(oppCatβπΆ) =
(oppCatβπΆ) |
4 | | eqid 2733 |
. . . . . . . . . 10
β’
(HomFβ(oppCatβπΆ)) =
(HomFβ(oppCatβπΆ)) |
5 | 1, 2, 3, 4 | yonval 18155 |
. . . . . . . . 9
β’ (π β π = (β¨πΆ, (oppCatβπΆ)β© curryF
(HomFβ(oppCatβπΆ)))) |
6 | 5 | fveq2d 6847 |
. . . . . . . 8
β’ (π β (1st
βπ) = (1st
β(β¨πΆ,
(oppCatβπΆ)β©
curryF (HomFβ(oppCatβπΆ))))) |
7 | 6 | fveq1d 6845 |
. . . . . . 7
β’ (π β ((1st
βπ)βπ) = ((1st
β(β¨πΆ,
(oppCatβπΆ)β©
curryF (HomFβ(oppCatβπΆ))))βπ)) |
8 | 7 | fveq2d 6847 |
. . . . . 6
β’ (π β (2nd
β((1st βπ)βπ)) = (2nd β((1st
β(β¨πΆ,
(oppCatβπΆ)β©
curryF (HomFβ(oppCatβπΆ))))βπ))) |
9 | 8 | oveqd 7375 |
. . . . 5
β’ (π β (π(2nd β((1st
βπ)βπ))π) = (π(2nd β((1st
β(β¨πΆ,
(oppCatβπΆ)β©
curryF (HomFβ(oppCatβπΆ))))βπ))π)) |
10 | 9 | fveq1d 6845 |
. . . 4
β’ (π β ((π(2nd β((1st
βπ)βπ))π)βπΉ) = ((π(2nd β((1st
β(β¨πΆ,
(oppCatβπΆ)β©
curryF (HomFβ(oppCatβπΆ))))βπ))π)βπΉ)) |
11 | | eqid 2733 |
. . . . 5
β’
(β¨πΆ,
(oppCatβπΆ)β©
curryF (HomFβ(oppCatβπΆ))) = (β¨πΆ, (oppCatβπΆ)β© curryF
(HomFβ(oppCatβπΆ))) |
12 | | yon11.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
13 | 3 | oppccat 17609 |
. . . . . 6
β’ (πΆ β Cat β
(oppCatβπΆ) β
Cat) |
14 | 2, 13 | syl 17 |
. . . . 5
β’ (π β (oppCatβπΆ) β Cat) |
15 | | eqid 2733 |
. . . . . 6
β’
(SetCatβran (Homf βπΆ)) = (SetCatβran
(Homf βπΆ)) |
16 | | fvex 6856 |
. . . . . . . 8
β’
(Homf βπΆ) β V |
17 | 16 | rnex 7850 |
. . . . . . 7
β’ ran
(Homf βπΆ) β V |
18 | 17 | a1i 11 |
. . . . . 6
β’ (π β ran
(Homf βπΆ) β V) |
19 | | ssidd 3968 |
. . . . . 6
β’ (π β ran
(Homf βπΆ) β ran (Homf
βπΆ)) |
20 | 3, 4, 15, 2, 18, 19 | oppchofcl 18154 |
. . . . 5
β’ (π β
(HomFβ(oppCatβπΆ)) β ((πΆ Γc
(oppCatβπΆ)) Func
(SetCatβran (Homf βπΆ)))) |
21 | 3, 12 | oppcbas 17604 |
. . . . 5
β’ π΅ =
(Baseβ(oppCatβπΆ)) |
22 | | yon11.p |
. . . . 5
β’ (π β π β π΅) |
23 | | eqid 2733 |
. . . . 5
β’
((1st β(β¨πΆ, (oppCatβπΆ)β© curryF
(HomFβ(oppCatβπΆ))))βπ) = ((1st β(β¨πΆ, (oppCatβπΆ)β© curryF
(HomFβ(oppCatβπΆ))))βπ) |
24 | | yon11.z |
. . . . 5
β’ (π β π β π΅) |
25 | | eqid 2733 |
. . . . 5
β’ (Hom
β(oppCatβπΆ)) =
(Hom β(oppCatβπΆ)) |
26 | | eqid 2733 |
. . . . 5
β’
(IdβπΆ) =
(IdβπΆ) |
27 | | yon12.w |
. . . . 5
β’ (π β π β π΅) |
28 | | yon12.f |
. . . . . 6
β’ (π β πΉ β (ππ»π)) |
29 | | yon11.h |
. . . . . . 7
β’ π» = (Hom βπΆ) |
30 | 29, 3 | oppchom 17601 |
. . . . . 6
β’ (π(Hom β(oppCatβπΆ))π) = (ππ»π) |
31 | 28, 30 | eleqtrrdi 2845 |
. . . . 5
β’ (π β πΉ β (π(Hom β(oppCatβπΆ))π)) |
32 | 11, 12, 2, 14, 20, 21, 22, 23, 24, 25, 26, 27, 31 | curf12 18121 |
. . . 4
β’ (π β ((π(2nd β((1st
β(β¨πΆ,
(oppCatβπΆ)β©
curryF (HomFβ(oppCatβπΆ))))βπ))π)βπΉ) = (((IdβπΆ)βπ)(β¨π, πβ©(2nd
β(HomFβ(oppCatβπΆ)))β¨π, πβ©)πΉ)) |
33 | 10, 32 | eqtrd 2773 |
. . 3
β’ (π β ((π(2nd β((1st
βπ)βπ))π)βπΉ) = (((IdβπΆ)βπ)(β¨π, πβ©(2nd
β(HomFβ(oppCatβπΆ)))β¨π, πβ©)πΉ)) |
34 | 33 | fveq1d 6845 |
. 2
β’ (π β (((π(2nd β((1st
βπ)βπ))π)βπΉ)βπΊ) = ((((IdβπΆ)βπ)(β¨π, πβ©(2nd
β(HomFβ(oppCatβπΆ)))β¨π, πβ©)πΉ)βπΊ)) |
35 | | eqid 2733 |
. . 3
β’
(compβ(oppCatβπΆ)) = (compβ(oppCatβπΆ)) |
36 | 12, 29, 26, 2, 22 | catidcl 17567 |
. . . 4
β’ (π β ((IdβπΆ)βπ) β (ππ»π)) |
37 | 29, 3 | oppchom 17601 |
. . . 4
β’ (π(Hom β(oppCatβπΆ))π) = (ππ»π) |
38 | 36, 37 | eleqtrrdi 2845 |
. . 3
β’ (π β ((IdβπΆ)βπ) β (π(Hom β(oppCatβπΆ))π)) |
39 | | yon12.g |
. . . 4
β’ (π β πΊ β (ππ»π)) |
40 | 29, 3 | oppchom 17601 |
. . . 4
β’ (π(Hom β(oppCatβπΆ))π) = (ππ»π) |
41 | 39, 40 | eleqtrrdi 2845 |
. . 3
β’ (π β πΊ β (π(Hom β(oppCatβπΆ))π)) |
42 | 4, 14, 21, 25, 22, 24, 22, 27, 35, 38, 31, 41 | hof2 18151 |
. 2
β’ (π β ((((IdβπΆ)βπ)(β¨π, πβ©(2nd
β(HomFβ(oppCatβπΆ)))β¨π, πβ©)πΉ)βπΊ) = ((πΉ(β¨π, πβ©(compβ(oppCatβπΆ))π)πΊ)(β¨π, πβ©(compβ(oppCatβπΆ))π)((IdβπΆ)βπ))) |
43 | | yon12.x |
. . . . 5
β’ Β· =
(compβπΆ) |
44 | 12, 43, 3, 22, 24, 27 | oppcco 17603 |
. . . 4
β’ (π β (πΉ(β¨π, πβ©(compβ(oppCatβπΆ))π)πΊ) = (πΊ(β¨π, πβ© Β· π)πΉ)) |
45 | 44 | oveq1d 7373 |
. . 3
β’ (π β ((πΉ(β¨π, πβ©(compβ(oppCatβπΆ))π)πΊ)(β¨π, πβ©(compβ(oppCatβπΆ))π)((IdβπΆ)βπ)) = ((πΊ(β¨π, πβ© Β· π)πΉ)(β¨π, πβ©(compβ(oppCatβπΆ))π)((IdβπΆ)βπ))) |
46 | 12, 43, 3, 22, 22, 27 | oppcco 17603 |
. . 3
β’ (π β ((πΊ(β¨π, πβ© Β· π)πΉ)(β¨π, πβ©(compβ(oppCatβπΆ))π)((IdβπΆ)βπ)) = (((IdβπΆ)βπ)(β¨π, πβ© Β· π)(πΊ(β¨π, πβ© Β· π)πΉ))) |
47 | 12, 29, 43, 2, 27, 24, 22, 28, 39 | catcocl 17570 |
. . . 4
β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) β (ππ»π)) |
48 | 12, 29, 26, 2, 27, 43, 22, 47 | catlid 17568 |
. . 3
β’ (π β (((IdβπΆ)βπ)(β¨π, πβ© Β· π)(πΊ(β¨π, πβ© Β· π)πΉ)) = (πΊ(β¨π, πβ© Β· π)πΉ)) |
49 | 45, 46, 48 | 3eqtrd 2777 |
. 2
β’ (π β ((πΉ(β¨π, πβ©(compβ(oppCatβπΆ))π)πΊ)(β¨π, πβ©(compβ(oppCatβπΆ))π)((IdβπΆ)βπ)) = (πΊ(β¨π, πβ© Β· π)πΉ)) |
50 | 34, 42, 49 | 3eqtrd 2777 |
1
β’ (π β (((π(2nd β((1st
βπ)βπ))π)βπΉ)βπΊ) = (πΊ(β¨π, πβ© Β· π)πΉ)) |