Step | Hyp | Ref
| Expression |
1 | | yoneda.z |
. . . . . 6
β’ π = (π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))) |
2 | 1 | fveq2i 6846 |
. . . . 5
β’
(1st βπ) = (1st β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))) |
3 | 2 | oveqi 7371 |
. . . 4
β’ (πΉ(1st βπ)π) = (πΉ(1st β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))π) |
4 | | df-ov 7361 |
. . . 4
β’ (πΉ(1st β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))π) = ((1st β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))ββ¨πΉ, πβ©) |
5 | 3, 4 | eqtri 2761 |
. . 3
β’ (πΉ(1st βπ)π) = ((1st β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))ββ¨πΉ, πβ©) |
6 | | eqid 2733 |
. . . . 5
β’ (π Γc
π) = (π Γc π) |
7 | | yoneda.q |
. . . . . 6
β’ π = (π FuncCat π) |
8 | 7 | fucbas 17853 |
. . . . 5
β’ (π Func π) = (Baseβπ) |
9 | | yoneda.o |
. . . . . 6
β’ π = (oppCatβπΆ) |
10 | | yoneda.b |
. . . . . 6
β’ π΅ = (BaseβπΆ) |
11 | 9, 10 | oppcbas 17604 |
. . . . 5
β’ π΅ = (Baseβπ) |
12 | 6, 8, 11 | xpcbas 18071 |
. . . 4
β’ ((π Func π) Γ π΅) = (Baseβ(π Γc π)) |
13 | | eqid 2733 |
. . . . 5
β’
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)) = ((β¨(1st
βπ), tpos
(2nd βπ)β© βfunc (π
2ndF π)) β¨,β©F (π
1stF π)) |
14 | | eqid 2733 |
. . . . 5
β’
((oppCatβπ)
Γc π) = ((oppCatβπ) Γc π) |
15 | | yoneda.c |
. . . . . . . . 9
β’ (π β πΆ β Cat) |
16 | 9 | oppccat 17609 |
. . . . . . . . 9
β’ (πΆ β Cat β π β Cat) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
β’ (π β π β Cat) |
18 | | yoneda.w |
. . . . . . . . . 10
β’ (π β π β π) |
19 | | yoneda.v |
. . . . . . . . . . 11
β’ (π β (ran
(Homf βπ) βͺ π) β π) |
20 | 19 | unssbd 4149 |
. . . . . . . . . 10
β’ (π β π β π) |
21 | 18, 20 | ssexd 5282 |
. . . . . . . . 9
β’ (π β π β V) |
22 | | yoneda.s |
. . . . . . . . . 10
β’ π = (SetCatβπ) |
23 | 22 | setccat 17976 |
. . . . . . . . 9
β’ (π β V β π β Cat) |
24 | 21, 23 | syl 17 |
. . . . . . . 8
β’ (π β π β Cat) |
25 | 7, 17, 24 | fuccat 17864 |
. . . . . . 7
β’ (π β π β Cat) |
26 | | eqid 2733 |
. . . . . . 7
β’ (π
2ndF π) = (π 2ndF π) |
27 | 6, 25, 17, 26 | 2ndfcl 18091 |
. . . . . 6
β’ (π β (π 2ndF π) β ((π Γc π) Func π)) |
28 | | eqid 2733 |
. . . . . . . 8
β’
(oppCatβπ) =
(oppCatβπ) |
29 | | relfunc 17753 |
. . . . . . . . 9
β’ Rel
(πΆ Func π) |
30 | | yoneda.y |
. . . . . . . . . 10
β’ π = (YonβπΆ) |
31 | | yoneda.u |
. . . . . . . . . 10
β’ (π β ran
(Homf βπΆ) β π) |
32 | 30, 15, 9, 22, 7, 21, 31 | yoncl 18156 |
. . . . . . . . 9
β’ (π β π β (πΆ Func π)) |
33 | | 1st2ndbr 7975 |
. . . . . . . . 9
β’ ((Rel
(πΆ Func π) β§ π β (πΆ Func π)) β (1st βπ)(πΆ Func π)(2nd βπ)) |
34 | 29, 32, 33 | sylancr 588 |
. . . . . . . 8
β’ (π β (1st
βπ)(πΆ Func π)(2nd βπ)) |
35 | 9, 28, 34 | funcoppc 17766 |
. . . . . . 7
β’ (π β (1st
βπ)(π Func (oppCatβπ))tpos (2nd βπ)) |
36 | | df-br 5107 |
. . . . . . 7
β’
((1st βπ)(π Func (oppCatβπ))tpos (2nd βπ) β β¨(1st
βπ), tpos
(2nd βπ)β© β (π Func (oppCatβπ))) |
37 | 35, 36 | sylib 217 |
. . . . . 6
β’ (π β β¨(1st
βπ), tpos
(2nd βπ)β© β (π Func (oppCatβπ))) |
38 | 27, 37 | cofucl 17779 |
. . . . 5
β’ (π β (β¨(1st
βπ), tpos
(2nd βπ)β© βfunc (π
2ndF π)) β ((π Γc π) Func (oppCatβπ))) |
39 | | eqid 2733 |
. . . . . 6
β’ (π
1stF π) = (π 1stF π) |
40 | 6, 25, 17, 39 | 1stfcl 18090 |
. . . . 5
β’ (π β (π 1stF π) β ((π Γc π) Func π)) |
41 | 13, 14, 38, 40 | prfcl 18096 |
. . . 4
β’ (π β ((β¨(1st
βπ), tpos
(2nd βπ)β© βfunc (π
2ndF π)) β¨,β©F (π
1stF π)) β ((π Γc π) Func ((oppCatβπ) Γc
π))) |
42 | | yoneda.h |
. . . . 5
β’ π» =
(HomFβπ) |
43 | | yoneda.t |
. . . . 5
β’ π = (SetCatβπ) |
44 | 19 | unssad 4148 |
. . . . 5
β’ (π β ran
(Homf βπ) β π) |
45 | 42, 28, 43, 25, 18, 44 | hofcl 18153 |
. . . 4
β’ (π β π» β (((oppCatβπ) Γc π) Func π)) |
46 | | yonedalem21.f |
. . . . 5
β’ (π β πΉ β (π Func π)) |
47 | | yonedalem21.x |
. . . . 5
β’ (π β π β π΅) |
48 | 46, 47 | opelxpd 5672 |
. . . 4
β’ (π β β¨πΉ, πβ© β ((π Func π) Γ π΅)) |
49 | 12, 41, 45, 48 | cofu1 17775 |
. . 3
β’ (π β ((1st
β(π»
βfunc ((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))ββ¨πΉ, πβ©) = ((1st βπ»)β((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©))) |
50 | 5, 49 | eqtrid 2785 |
. 2
β’ (π β (πΉ(1st βπ)π) = ((1st βπ»)β((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©))) |
51 | | eqid 2733 |
. . . . . 6
β’ (Hom
β(π
Γc π)) = (Hom β(π Γc π)) |
52 | 13, 12, 51, 38, 40, 48 | prf1 18093 |
. . . . 5
β’ (π β ((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©) = β¨((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΉ, πβ©), ((1st β(π
1stF π))ββ¨πΉ, πβ©)β©) |
53 | 12, 27, 37, 48 | cofu1 17775 |
. . . . . . 7
β’ (π β ((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΉ, πβ©) = ((1st
ββ¨(1st βπ), tpos (2nd βπ)β©)β((1st
β(π
2ndF π))ββ¨πΉ, πβ©))) |
54 | | fvex 6856 |
. . . . . . . . . 10
β’
(1st βπ) β V |
55 | | fvex 6856 |
. . . . . . . . . . 11
β’
(2nd βπ) β V |
56 | 55 | tposex 8192 |
. . . . . . . . . 10
β’ tpos
(2nd βπ)
β V |
57 | 54, 56 | op1st 7930 |
. . . . . . . . 9
β’
(1st ββ¨(1st βπ), tpos (2nd βπ)β©) = (1st
βπ) |
58 | 57 | a1i 11 |
. . . . . . . 8
β’ (π β (1st
ββ¨(1st βπ), tpos (2nd βπ)β©) = (1st
βπ)) |
59 | 6, 12, 51, 25, 17, 26, 48 | 2ndf1 18088 |
. . . . . . . . 9
β’ (π β ((1st
β(π
2ndF π))ββ¨πΉ, πβ©) = (2nd ββ¨πΉ, πβ©)) |
60 | | op2ndg 7935 |
. . . . . . . . . 10
β’ ((πΉ β (π Func π) β§ π β π΅) β (2nd ββ¨πΉ, πβ©) = π) |
61 | 46, 47, 60 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (2nd
ββ¨πΉ, πβ©) = π) |
62 | 59, 61 | eqtrd 2773 |
. . . . . . . 8
β’ (π β ((1st
β(π
2ndF π))ββ¨πΉ, πβ©) = π) |
63 | 58, 62 | fveq12d 6850 |
. . . . . . 7
β’ (π β ((1st
ββ¨(1st βπ), tpos (2nd βπ)β©)β((1st
β(π
2ndF π))ββ¨πΉ, πβ©)) = ((1st βπ)βπ)) |
64 | 53, 63 | eqtrd 2773 |
. . . . . 6
β’ (π β ((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΉ, πβ©) = ((1st βπ)βπ)) |
65 | 6, 12, 51, 25, 17, 39, 48 | 1stf1 18085 |
. . . . . . 7
β’ (π β ((1st
β(π
1stF π))ββ¨πΉ, πβ©) = (1st ββ¨πΉ, πβ©)) |
66 | | op1stg 7934 |
. . . . . . . 8
β’ ((πΉ β (π Func π) β§ π β π΅) β (1st ββ¨πΉ, πβ©) = πΉ) |
67 | 46, 47, 66 | syl2anc 585 |
. . . . . . 7
β’ (π β (1st
ββ¨πΉ, πβ©) = πΉ) |
68 | 65, 67 | eqtrd 2773 |
. . . . . 6
β’ (π β ((1st
β(π
1stF π))ββ¨πΉ, πβ©) = πΉ) |
69 | 64, 68 | opeq12d 4839 |
. . . . 5
β’ (π β β¨((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΉ, πβ©), ((1st β(π
1stF π))ββ¨πΉ, πβ©)β© = β¨((1st
βπ)βπ), πΉβ©) |
70 | 52, 69 | eqtrd 2773 |
. . . 4
β’ (π β ((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©) = β¨((1st
βπ)βπ), πΉβ©) |
71 | 70 | fveq2d 6847 |
. . 3
β’ (π β ((1st
βπ»)β((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©)) = ((1st βπ»)ββ¨((1st
βπ)βπ), πΉβ©)) |
72 | | df-ov 7361 |
. . 3
β’
(((1st βπ)βπ)(1st βπ»)πΉ) = ((1st βπ»)ββ¨((1st
βπ)βπ), πΉβ©) |
73 | 71, 72 | eqtr4di 2791 |
. 2
β’ (π β ((1st
βπ»)β((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©)) = (((1st βπ)βπ)(1st βπ»)πΉ)) |
74 | | eqid 2733 |
. . . 4
β’ (π Nat π) = (π Nat π) |
75 | 7, 74 | fuchom 17854 |
. . 3
β’ (π Nat π) = (Hom βπ) |
76 | 30, 10, 15, 47, 9, 22, 21, 31 | yon1cl 18157 |
. . 3
β’ (π β ((1st
βπ)βπ) β (π Func π)) |
77 | 42, 25, 8, 75, 76, 46 | hof1 18148 |
. 2
β’ (π β (((1st
βπ)βπ)(1st βπ»)πΉ) = (((1st βπ)βπ)(π Nat π)πΉ)) |
78 | 50, 73, 77 | 3eqtrd 2777 |
1
β’ (π β (πΉ(1st βπ)π) = (((1st βπ)βπ)(π Nat π)πΉ)) |