Step | Hyp | Ref
| Expression |
1 | | yoneda.z |
. . . . . . 7
β’ π = (π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))) |
2 | 1 | fveq2i 6892 |
. . . . . 6
β’
(2nd βπ) = (2nd β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))) |
3 | 2 | oveqi 7419 |
. . . . 5
β’
(β¨πΉ, πβ©(2nd
βπ)β¨πΊ, πβ©) = (β¨πΉ, πβ©(2nd β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))β¨πΊ, πβ©) |
4 | 3 | oveqi 7419 |
. . . 4
β’ (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) = (π΄(β¨πΉ, πβ©(2nd β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))β¨πΊ, πβ©)πΎ) |
5 | | df-ov 7409 |
. . . 4
β’ (π΄(β¨πΉ, πβ©(2nd β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))β¨πΊ, πβ©)πΎ) = ((β¨πΉ, πβ©(2nd β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) |
6 | 4, 5 | eqtri 2761 |
. . 3
β’ (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) = ((β¨πΉ, πβ©(2nd β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) |
7 | | eqid 2733 |
. . . . 5
β’ (π Γc
π) = (π Γc π) |
8 | | yoneda.q |
. . . . . 6
β’ π = (π FuncCat π) |
9 | 8 | fucbas 17909 |
. . . . 5
β’ (π Func π) = (Baseβπ) |
10 | | yoneda.o |
. . . . . 6
β’ π = (oppCatβπΆ) |
11 | | yoneda.b |
. . . . . 6
β’ π΅ = (BaseβπΆ) |
12 | 10, 11 | oppcbas 17660 |
. . . . 5
β’ π΅ = (Baseβπ) |
13 | 7, 9, 12 | xpcbas 18127 |
. . . 4
β’ ((π Func π) Γ π΅) = (Baseβ(π Γc π)) |
14 | | eqid 2733 |
. . . . 5
β’
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)) = ((β¨(1st
βπ), tpos
(2nd βπ)β© βfunc (π
2ndF π)) β¨,β©F (π
1stF π)) |
15 | | eqid 2733 |
. . . . 5
β’
((oppCatβπ)
Γc π) = ((oppCatβπ) Γc π) |
16 | | yoneda.c |
. . . . . . . . 9
β’ (π β πΆ β Cat) |
17 | 10 | oppccat 17665 |
. . . . . . . . 9
β’ (πΆ β Cat β π β Cat) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
β’ (π β π β Cat) |
19 | | yoneda.w |
. . . . . . . . . 10
β’ (π β π β π) |
20 | | yoneda.v |
. . . . . . . . . . 11
β’ (π β (ran
(Homf βπ) βͺ π) β π) |
21 | 20 | unssbd 4188 |
. . . . . . . . . 10
β’ (π β π β π) |
22 | 19, 21 | ssexd 5324 |
. . . . . . . . 9
β’ (π β π β V) |
23 | | yoneda.s |
. . . . . . . . . 10
β’ π = (SetCatβπ) |
24 | 23 | setccat 18032 |
. . . . . . . . 9
β’ (π β V β π β Cat) |
25 | 22, 24 | syl 17 |
. . . . . . . 8
β’ (π β π β Cat) |
26 | 8, 18, 25 | fuccat 17920 |
. . . . . . 7
β’ (π β π β Cat) |
27 | | eqid 2733 |
. . . . . . 7
β’ (π
2ndF π) = (π 2ndF π) |
28 | 7, 26, 18, 27 | 2ndfcl 18147 |
. . . . . 6
β’ (π β (π 2ndF π) β ((π Γc π) Func π)) |
29 | | eqid 2733 |
. . . . . . . 8
β’
(oppCatβπ) =
(oppCatβπ) |
30 | | relfunc 17809 |
. . . . . . . . 9
β’ Rel
(πΆ Func π) |
31 | | yoneda.y |
. . . . . . . . . 10
β’ π = (YonβπΆ) |
32 | | yoneda.u |
. . . . . . . . . 10
β’ (π β ran
(Homf βπΆ) β π) |
33 | 31, 16, 10, 23, 8, 22, 32 | yoncl 18212 |
. . . . . . . . 9
β’ (π β π β (πΆ Func π)) |
34 | | 1st2ndbr 8025 |
. . . . . . . . 9
β’ ((Rel
(πΆ Func π) β§ π β (πΆ Func π)) β (1st βπ)(πΆ Func π)(2nd βπ)) |
35 | 30, 33, 34 | sylancr 588 |
. . . . . . . 8
β’ (π β (1st
βπ)(πΆ Func π)(2nd βπ)) |
36 | 10, 29, 35 | funcoppc 17822 |
. . . . . . 7
β’ (π β (1st
βπ)(π Func (oppCatβπ))tpos (2nd βπ)) |
37 | | df-br 5149 |
. . . . . . 7
β’
((1st βπ)(π Func (oppCatβπ))tpos (2nd βπ) β β¨(1st
βπ), tpos
(2nd βπ)β© β (π Func (oppCatβπ))) |
38 | 36, 37 | sylib 217 |
. . . . . 6
β’ (π β β¨(1st
βπ), tpos
(2nd βπ)β© β (π Func (oppCatβπ))) |
39 | 28, 38 | cofucl 17835 |
. . . . 5
β’ (π β (β¨(1st
βπ), tpos
(2nd βπ)β© βfunc (π
2ndF π)) β ((π Γc π) Func (oppCatβπ))) |
40 | | eqid 2733 |
. . . . . 6
β’ (π
1stF π) = (π 1stF π) |
41 | 7, 26, 18, 40 | 1stfcl 18146 |
. . . . 5
β’ (π β (π 1stF π) β ((π Γc π) Func π)) |
42 | 14, 15, 39, 41 | prfcl 18152 |
. . . 4
β’ (π β ((β¨(1st
βπ), tpos
(2nd βπ)β© βfunc (π
2ndF π)) β¨,β©F (π
1stF π)) β ((π Γc π) Func ((oppCatβπ) Γc
π))) |
43 | | yoneda.h |
. . . . 5
β’ π» =
(HomFβπ) |
44 | | yoneda.t |
. . . . 5
β’ π = (SetCatβπ) |
45 | 20 | unssad 4187 |
. . . . 5
β’ (π β ran
(Homf βπ) β π) |
46 | 43, 29, 44, 26, 19, 45 | hofcl 18209 |
. . . 4
β’ (π β π» β (((oppCatβπ) Γc π) Func π)) |
47 | | yonedalem21.f |
. . . . 5
β’ (π β πΉ β (π Func π)) |
48 | | yonedalem21.x |
. . . . 5
β’ (π β π β π΅) |
49 | 47, 48 | opelxpd 5714 |
. . . 4
β’ (π β β¨πΉ, πβ© β ((π Func π) Γ π΅)) |
50 | | yonedalem22.g |
. . . . 5
β’ (π β πΊ β (π Func π)) |
51 | | yonedalem22.p |
. . . . 5
β’ (π β π β π΅) |
52 | 50, 51 | opelxpd 5714 |
. . . 4
β’ (π β β¨πΊ, πβ© β ((π Func π) Γ π΅)) |
53 | | eqid 2733 |
. . . 4
β’ (Hom
β(π
Γc π)) = (Hom β(π Γc π)) |
54 | | yonedalem22.a |
. . . . . 6
β’ (π β π΄ β (πΉ(π Nat π)πΊ)) |
55 | | yonedalem22.k |
. . . . . . 7
β’ (π β πΎ β (π(Hom βπΆ)π)) |
56 | | eqid 2733 |
. . . . . . . 8
β’ (Hom
βπΆ) = (Hom
βπΆ) |
57 | 56, 10 | oppchom 17657 |
. . . . . . 7
β’ (π(Hom βπ)π) = (π(Hom βπΆ)π) |
58 | 55, 57 | eleqtrrdi 2845 |
. . . . . 6
β’ (π β πΎ β (π(Hom βπ)π)) |
59 | 54, 58 | opelxpd 5714 |
. . . . 5
β’ (π β β¨π΄, πΎβ© β ((πΉ(π Nat π)πΊ) Γ (π(Hom βπ)π))) |
60 | | eqid 2733 |
. . . . . . 7
β’ (π Nat π) = (π Nat π) |
61 | 8, 60 | fuchom 17910 |
. . . . . 6
β’ (π Nat π) = (Hom βπ) |
62 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπ) = (Hom
βπ) |
63 | 7, 9, 12, 61, 62, 47, 48, 50, 51, 53 | xpchom2 18135 |
. . . . 5
β’ (π β (β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©) = ((πΉ(π Nat π)πΊ) Γ (π(Hom βπ)π))) |
64 | 59, 63 | eleqtrrd 2837 |
. . . 4
β’ (π β β¨π΄, πΎβ© β (β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©)) |
65 | 13, 42, 46, 49, 52, 53, 64 | cofu2 17833 |
. . 3
β’ (π β ((β¨πΉ, πβ©(2nd β(π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = ((((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©)(2nd βπ»)((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΊ, πβ©))β((β¨πΉ, πβ©(2nd
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©))) |
66 | 6, 65 | eqtrid 2785 |
. 2
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) = ((((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©)(2nd βπ»)((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΊ, πβ©))β((β¨πΉ, πβ©(2nd
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©))) |
67 | 14, 13, 53, 39, 41, 49 | prf1 18149 |
. . . . . 6
β’ (π β ((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©) = β¨((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΉ, πβ©), ((1st β(π
1stF π))ββ¨πΉ, πβ©)β©) |
68 | 13, 28, 38, 49 | cofu1 17831 |
. . . . . . . 8
β’ (π β ((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΉ, πβ©) = ((1st
ββ¨(1st βπ), tpos (2nd βπ)β©)β((1st
β(π
2ndF π))ββ¨πΉ, πβ©))) |
69 | | fvex 6902 |
. . . . . . . . . . 11
β’
(1st βπ) β V |
70 | | fvex 6902 |
. . . . . . . . . . . 12
β’
(2nd βπ) β V |
71 | 70 | tposex 8242 |
. . . . . . . . . . 11
β’ tpos
(2nd βπ)
β V |
72 | 69, 71 | op1st 7980 |
. . . . . . . . . 10
β’
(1st ββ¨(1st βπ), tpos (2nd βπ)β©) = (1st
βπ) |
73 | 72 | a1i 11 |
. . . . . . . . 9
β’ (π β (1st
ββ¨(1st βπ), tpos (2nd βπ)β©) = (1st
βπ)) |
74 | 7, 13, 53, 26, 18, 27, 49 | 2ndf1 18144 |
. . . . . . . . . 10
β’ (π β ((1st
β(π
2ndF π))ββ¨πΉ, πβ©) = (2nd ββ¨πΉ, πβ©)) |
75 | | op2ndg 7985 |
. . . . . . . . . . 11
β’ ((πΉ β (π Func π) β§ π β π΅) β (2nd ββ¨πΉ, πβ©) = π) |
76 | 47, 48, 75 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (2nd
ββ¨πΉ, πβ©) = π) |
77 | 74, 76 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β ((1st
β(π
2ndF π))ββ¨πΉ, πβ©) = π) |
78 | 73, 77 | fveq12d 6896 |
. . . . . . . 8
β’ (π β ((1st
ββ¨(1st βπ), tpos (2nd βπ)β©)β((1st
β(π
2ndF π))ββ¨πΉ, πβ©)) = ((1st βπ)βπ)) |
79 | 68, 78 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΉ, πβ©) = ((1st βπ)βπ)) |
80 | 7, 13, 53, 26, 18, 40, 49 | 1stf1 18141 |
. . . . . . . 8
β’ (π β ((1st
β(π
1stF π))ββ¨πΉ, πβ©) = (1st ββ¨πΉ, πβ©)) |
81 | | op1stg 7984 |
. . . . . . . . 9
β’ ((πΉ β (π Func π) β§ π β π΅) β (1st ββ¨πΉ, πβ©) = πΉ) |
82 | 47, 48, 81 | syl2anc 585 |
. . . . . . . 8
β’ (π β (1st
ββ¨πΉ, πβ©) = πΉ) |
83 | 80, 82 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((1st
β(π
1stF π))ββ¨πΉ, πβ©) = πΉ) |
84 | 79, 83 | opeq12d 4881 |
. . . . . 6
β’ (π β β¨((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΉ, πβ©), ((1st β(π
1stF π))ββ¨πΉ, πβ©)β© = β¨((1st
βπ)βπ), πΉβ©) |
85 | 67, 84 | eqtrd 2773 |
. . . . 5
β’ (π β ((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©) = β¨((1st
βπ)βπ), πΉβ©) |
86 | 14, 13, 53, 39, 41, 52 | prf1 18149 |
. . . . . 6
β’ (π β ((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΊ, πβ©) = β¨((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΊ, πβ©), ((1st β(π
1stF π))ββ¨πΊ, πβ©)β©) |
87 | 13, 28, 38, 52 | cofu1 17831 |
. . . . . . . 8
β’ (π β ((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΊ, πβ©) = ((1st
ββ¨(1st βπ), tpos (2nd βπ)β©)β((1st
β(π
2ndF π))ββ¨πΊ, πβ©))) |
88 | 7, 13, 53, 26, 18, 27, 52 | 2ndf1 18144 |
. . . . . . . . . 10
β’ (π β ((1st
β(π
2ndF π))ββ¨πΊ, πβ©) = (2nd ββ¨πΊ, πβ©)) |
89 | | op2ndg 7985 |
. . . . . . . . . . 11
β’ ((πΊ β (π Func π) β§ π β π΅) β (2nd ββ¨πΊ, πβ©) = π) |
90 | 50, 51, 89 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (2nd
ββ¨πΊ, πβ©) = π) |
91 | 88, 90 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β ((1st
β(π
2ndF π))ββ¨πΊ, πβ©) = π) |
92 | 73, 91 | fveq12d 6896 |
. . . . . . . 8
β’ (π β ((1st
ββ¨(1st βπ), tpos (2nd βπ)β©)β((1st
β(π
2ndF π))ββ¨πΊ, πβ©)) = ((1st βπ)βπ)) |
93 | 87, 92 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΊ, πβ©) = ((1st βπ)βπ)) |
94 | 7, 13, 53, 26, 18, 40, 52 | 1stf1 18141 |
. . . . . . . 8
β’ (π β ((1st
β(π
1stF π))ββ¨πΊ, πβ©) = (1st ββ¨πΊ, πβ©)) |
95 | | op1stg 7984 |
. . . . . . . . 9
β’ ((πΊ β (π Func π) β§ π β π΅) β (1st ββ¨πΊ, πβ©) = πΊ) |
96 | 50, 51, 95 | syl2anc 585 |
. . . . . . . 8
β’ (π β (1st
ββ¨πΊ, πβ©) = πΊ) |
97 | 94, 96 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((1st
β(π
1stF π))ββ¨πΊ, πβ©) = πΊ) |
98 | 93, 97 | opeq12d 4881 |
. . . . . 6
β’ (π β β¨((1st
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))ββ¨πΊ, πβ©), ((1st β(π
1stF π))ββ¨πΊ, πβ©)β© = β¨((1st
βπ)βπ), πΊβ©) |
99 | 86, 98 | eqtrd 2773 |
. . . . 5
β’ (π β ((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΊ, πβ©) = β¨((1st
βπ)βπ), πΊβ©) |
100 | 85, 99 | oveq12d 7424 |
. . . 4
β’ (π β (((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©)(2nd βπ»)((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΊ, πβ©)) = (β¨((1st
βπ)βπ), πΉβ©(2nd βπ»)β¨((1st
βπ)βπ), πΊβ©)) |
101 | 14, 13, 53, 39, 41, 49, 52, 64 | prf2 18151 |
. . . . 5
β’ (π β ((β¨πΉ, πβ©(2nd
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = β¨((β¨πΉ, πβ©(2nd
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©), ((β¨πΉ, πβ©(2nd β(π
1stF π))β¨πΊ, πβ©)ββ¨π΄, πΎβ©)β©) |
102 | 13, 28, 38, 49, 52, 53, 64 | cofu2 17833 |
. . . . . . 7
β’ (π β ((β¨πΉ, πβ©(2nd
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = ((((1st β(π
2ndF π))ββ¨πΉ, πβ©)(2nd
ββ¨(1st βπ), tpos (2nd βπ)β©)((1st
β(π
2ndF π))ββ¨πΊ, πβ©))β((β¨πΉ, πβ©(2nd β(π
2ndF π))β¨πΊ, πβ©)ββ¨π΄, πΎβ©))) |
103 | 69, 71 | op2nd 7981 |
. . . . . . . . . . 11
β’
(2nd ββ¨(1st βπ), tpos (2nd βπ)β©) = tpos (2nd
βπ) |
104 | 103 | oveqi 7419 |
. . . . . . . . . 10
β’
(((1st β(π 2ndF π))ββ¨πΉ, πβ©)(2nd
ββ¨(1st βπ), tpos (2nd βπ)β©)((1st
β(π
2ndF π))ββ¨πΊ, πβ©)) = (((1st β(π
2ndF π))ββ¨πΉ, πβ©)tpos (2nd βπ)((1st β(π
2ndF π))ββ¨πΊ, πβ©)) |
105 | | ovtpos 8223 |
. . . . . . . . . 10
β’
(((1st β(π 2ndF π))ββ¨πΉ, πβ©)tpos (2nd βπ)((1st β(π
2ndF π))ββ¨πΊ, πβ©)) = (((1st β(π
2ndF π))ββ¨πΊ, πβ©)(2nd βπ)((1st β(π
2ndF π))ββ¨πΉ, πβ©)) |
106 | 104, 105 | eqtri 2761 |
. . . . . . . . 9
β’
(((1st β(π 2ndF π))ββ¨πΉ, πβ©)(2nd
ββ¨(1st βπ), tpos (2nd βπ)β©)((1st
β(π
2ndF π))ββ¨πΊ, πβ©)) = (((1st β(π
2ndF π))ββ¨πΊ, πβ©)(2nd βπ)((1st β(π
2ndF π))ββ¨πΉ, πβ©)) |
107 | 91, 77 | oveq12d 7424 |
. . . . . . . . 9
β’ (π β (((1st
β(π
2ndF π))ββ¨πΊ, πβ©)(2nd βπ)((1st β(π
2ndF π))ββ¨πΉ, πβ©)) = (π(2nd βπ)π)) |
108 | 106, 107 | eqtrid 2785 |
. . . . . . . 8
β’ (π β (((1st
β(π
2ndF π))ββ¨πΉ, πβ©)(2nd
ββ¨(1st βπ), tpos (2nd βπ)β©)((1st
β(π
2ndF π))ββ¨πΊ, πβ©)) = (π(2nd βπ)π)) |
109 | 7, 13, 53, 26, 18, 27, 49, 52 | 2ndf2 18145 |
. . . . . . . . . 10
β’ (π β (β¨πΉ, πβ©(2nd β(π
2ndF π))β¨πΊ, πβ©) = (2nd βΎ
(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©))) |
110 | 109 | fveq1d 6891 |
. . . . . . . . 9
β’ (π β ((β¨πΉ, πβ©(2nd β(π
2ndF π))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = ((2nd βΎ
(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©))ββ¨π΄, πΎβ©)) |
111 | 64 | fvresd 6909 |
. . . . . . . . 9
β’ (π β ((2nd βΎ
(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©))ββ¨π΄, πΎβ©) = (2nd ββ¨π΄, πΎβ©)) |
112 | | op2ndg 7985 |
. . . . . . . . . 10
β’ ((π΄ β (πΉ(π Nat π)πΊ) β§ πΎ β (π(Hom βπΆ)π)) β (2nd ββ¨π΄, πΎβ©) = πΎ) |
113 | 54, 55, 112 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (2nd
ββ¨π΄, πΎβ©) = πΎ) |
114 | 110, 111,
113 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β ((β¨πΉ, πβ©(2nd β(π
2ndF π))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = πΎ) |
115 | 108, 114 | fveq12d 6896 |
. . . . . . 7
β’ (π β ((((1st
β(π
2ndF π))ββ¨πΉ, πβ©)(2nd
ββ¨(1st βπ), tpos (2nd βπ)β©)((1st
β(π
2ndF π))ββ¨πΊ, πβ©))β((β¨πΉ, πβ©(2nd β(π
2ndF π))β¨πΊ, πβ©)ββ¨π΄, πΎβ©)) = ((π(2nd βπ)π)βπΎ)) |
116 | 102, 115 | eqtrd 2773 |
. . . . . 6
β’ (π β ((β¨πΉ, πβ©(2nd
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = ((π(2nd βπ)π)βπΎ)) |
117 | 7, 13, 53, 26, 18, 40, 49, 52 | 1stf2 18142 |
. . . . . . . 8
β’ (π β (β¨πΉ, πβ©(2nd β(π
1stF π))β¨πΊ, πβ©) = (1st βΎ
(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©))) |
118 | 117 | fveq1d 6891 |
. . . . . . 7
β’ (π β ((β¨πΉ, πβ©(2nd β(π
1stF π))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = ((1st βΎ
(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©))ββ¨π΄, πΎβ©)) |
119 | 64 | fvresd 6909 |
. . . . . . 7
β’ (π β ((1st βΎ
(β¨πΉ, πβ©(Hom β(π Γc π))β¨πΊ, πβ©))ββ¨π΄, πΎβ©) = (1st ββ¨π΄, πΎβ©)) |
120 | | op1stg 7984 |
. . . . . . . 8
β’ ((π΄ β (πΉ(π Nat π)πΊ) β§ πΎ β (π(Hom βπΆ)π)) β (1st ββ¨π΄, πΎβ©) = π΄) |
121 | 54, 55, 120 | syl2anc 585 |
. . . . . . 7
β’ (π β (1st
ββ¨π΄, πΎβ©) = π΄) |
122 | 118, 119,
121 | 3eqtrd 2777 |
. . . . . 6
β’ (π β ((β¨πΉ, πβ©(2nd β(π
1stF π))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = π΄) |
123 | 116, 122 | opeq12d 4881 |
. . . . 5
β’ (π β β¨((β¨πΉ, πβ©(2nd
β(β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©), ((β¨πΉ, πβ©(2nd β(π
1stF π))β¨πΊ, πβ©)ββ¨π΄, πΎβ©)β© = β¨((π(2nd βπ)π)βπΎ), π΄β©) |
124 | 101, 123 | eqtrd 2773 |
. . . 4
β’ (π β ((β¨πΉ, πβ©(2nd
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©) = β¨((π(2nd βπ)π)βπΎ), π΄β©) |
125 | 100, 124 | fveq12d 6896 |
. . 3
β’ (π β ((((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©)(2nd βπ»)((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΊ, πβ©))β((β¨πΉ, πβ©(2nd
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©)) = ((β¨((1st
βπ)βπ), πΉβ©(2nd βπ»)β¨((1st
βπ)βπ), πΊβ©)ββ¨((π(2nd βπ)π)βπΎ), π΄β©)) |
126 | | df-ov 7409 |
. . 3
β’ (((π(2nd βπ)π)βπΎ)(β¨((1st βπ)βπ), πΉβ©(2nd βπ»)β¨((1st
βπ)βπ), πΊβ©)π΄) = ((β¨((1st βπ)βπ), πΉβ©(2nd βπ»)β¨((1st
βπ)βπ), πΊβ©)ββ¨((π(2nd βπ)π)βπΎ), π΄β©) |
127 | 125, 126 | eqtr4di 2791 |
. 2
β’ (π β ((((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΉ, πβ©)(2nd βπ»)((1st
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))ββ¨πΊ, πβ©))β((β¨πΉ, πβ©(2nd
β((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π)))β¨πΊ, πβ©)ββ¨π΄, πΎβ©)) = (((π(2nd βπ)π)βπΎ)(β¨((1st βπ)βπ), πΉβ©(2nd βπ»)β¨((1st
βπ)βπ), πΊβ©)π΄)) |
128 | 66, 127 | eqtrd 2773 |
1
β’ (π β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) = (((π(2nd βπ)π)βπΎ)(β¨((1st βπ)βπ), πΉβ©(2nd βπ»)β¨((1st
βπ)βπ), πΊβ©)π΄)) |