Step | Hyp | Ref
| Expression |
1 | | yoneda.m |
. . . . 5
β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) |
2 | | ovex 7394 |
. . . . . 6
β’
(((1st βπ)βπ₯)(π Nat π)π) β V |
3 | 2 | mptex 7177 |
. . . . 5
β’ (π β (((1st
βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯))) β V |
4 | 1, 3 | fnmpoi 8006 |
. . . 4
β’ π Fn ((π Func π) Γ π΅) |
5 | 4 | a1i 11 |
. . 3
β’ (π β π Fn ((π Func π) Γ π΅)) |
6 | | yoneda.y |
. . . . . . . 8
β’ π = (YonβπΆ) |
7 | | yoneda.b |
. . . . . . . 8
β’ π΅ = (BaseβπΆ) |
8 | | yoneda.1 |
. . . . . . . 8
β’ 1 =
(IdβπΆ) |
9 | | yoneda.o |
. . . . . . . 8
β’ π = (oppCatβπΆ) |
10 | | yoneda.s |
. . . . . . . 8
β’ π = (SetCatβπ) |
11 | | yoneda.t |
. . . . . . . 8
β’ π = (SetCatβπ) |
12 | | yoneda.q |
. . . . . . . 8
β’ π = (π FuncCat π) |
13 | | yoneda.h |
. . . . . . . 8
β’ π» =
(HomFβπ) |
14 | | yoneda.r |
. . . . . . . 8
β’ π
= ((π Γc π) FuncCat π) |
15 | | yoneda.e |
. . . . . . . 8
β’ πΈ = (π evalF π) |
16 | | yoneda.z |
. . . . . . . 8
β’ π = (π» βfunc
((β¨(1st βπ), tpos (2nd βπ)β©
βfunc (π 2ndF π))
β¨,β©F (π 1stF π))) |
17 | | yoneda.c |
. . . . . . . . 9
β’ (π β πΆ β Cat) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β πΆ β Cat) |
19 | | yoneda.w |
. . . . . . . . 9
β’ (π β π β π) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β π β π) |
21 | | yoneda.u |
. . . . . . . . 9
β’ (π β ran
(Homf βπΆ) β π) |
22 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β ran (Homf
βπΆ) β π) |
23 | | yoneda.v |
. . . . . . . . 9
β’ (π β (ran
(Homf βπ) βͺ π) β π) |
24 | 23 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β (ran (Homf
βπ) βͺ π) β π) |
25 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β π β (π Func π)) |
26 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β π¦ β π΅) |
27 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 18, 20, 22, 24, 25, 26, 1 | yonedalem3a 18171 |
. . . . . . 7
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β ((πππ¦) = (π β (((1st βπ)βπ¦)(π Nat π)π) β¦ ((πβπ¦)β( 1 βπ¦))) β§ (πππ¦):(π(1st βπ)π¦)βΆ(π(1st βπΈ)π¦))) |
28 | 27 | simprd 497 |
. . . . . 6
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β (πππ¦):(π(1st βπ)π¦)βΆ(π(1st βπΈ)π¦)) |
29 | | eqid 2733 |
. . . . . . 7
β’ (Hom
βπ) = (Hom
βπ) |
30 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π Γc
π) = (π Γc π) |
31 | 12 | fucbas 17856 |
. . . . . . . . . . 11
β’ (π Func π) = (Baseβπ) |
32 | 9, 7 | oppcbas 17607 |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ) |
33 | 30, 31, 32 | xpcbas 18074 |
. . . . . . . . . 10
β’ ((π Func π) Γ π΅) = (Baseβ(π Γc π)) |
34 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
35 | | relfunc 17756 |
. . . . . . . . . . 11
β’ Rel
((π
Γc π) Func π) |
36 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 19, 21, 23 | yonedalem1 18169 |
. . . . . . . . . . . 12
β’ (π β (π β ((π Γc π) Func π) β§ πΈ β ((π Γc π) Func π))) |
37 | 36 | simpld 496 |
. . . . . . . . . . 11
β’ (π β π β ((π Γc π) Func π)) |
38 | | 1st2ndbr 7978 |
. . . . . . . . . . 11
β’ ((Rel
((π
Γc π) Func π) β§ π β ((π Γc π) Func π)) β (1st βπ)((π Γc π) Func π)(2nd βπ)) |
39 | 35, 37, 38 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (1st
βπ)((π Γc
π) Func π)(2nd βπ)) |
40 | 33, 34, 39 | funcf1 17760 |
. . . . . . . . 9
β’ (π β (1st
βπ):((π Func π) Γ π΅)βΆ(Baseβπ)) |
41 | 40 | fovcdmda 7529 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β (π(1st βπ)π¦) β (Baseβπ)) |
42 | 11, 20 | setcbas 17972 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β π = (Baseβπ)) |
43 | 41, 42 | eleqtrrd 2837 |
. . . . . . 7
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β (π(1st βπ)π¦) β π) |
44 | 36 | simprd 497 |
. . . . . . . . . . 11
β’ (π β πΈ β ((π Γc π) Func π)) |
45 | | 1st2ndbr 7978 |
. . . . . . . . . . 11
β’ ((Rel
((π
Γc π) Func π) β§ πΈ β ((π Γc π) Func π)) β (1st βπΈ)((π Γc π) Func π)(2nd βπΈ)) |
46 | 35, 44, 45 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (1st
βπΈ)((π Γc
π) Func π)(2nd βπΈ)) |
47 | 33, 34, 46 | funcf1 17760 |
. . . . . . . . 9
β’ (π β (1st
βπΈ):((π Func π) Γ π΅)βΆ(Baseβπ)) |
48 | 47 | fovcdmda 7529 |
. . . . . . . 8
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β (π(1st βπΈ)π¦) β (Baseβπ)) |
49 | 48, 42 | eleqtrrd 2837 |
. . . . . . 7
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β (π(1st βπΈ)π¦) β π) |
50 | 11, 20, 29, 43, 49 | elsetchom 17975 |
. . . . . 6
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β ((πππ¦) β ((π(1st βπ)π¦)(Hom βπ)(π(1st βπΈ)π¦)) β (πππ¦):(π(1st βπ)π¦)βΆ(π(1st βπΈ)π¦))) |
51 | 28, 50 | mpbird 257 |
. . . . 5
β’ ((π β§ (π β (π Func π) β§ π¦ β π΅)) β (πππ¦) β ((π(1st βπ)π¦)(Hom βπ)(π(1st βπΈ)π¦))) |
52 | 51 | ralrimivva 3194 |
. . . 4
β’ (π β βπ β (π Func π)βπ¦ β π΅ (πππ¦) β ((π(1st βπ)π¦)(Hom βπ)(π(1st βπΈ)π¦))) |
53 | | fveq2 6846 |
. . . . . . 7
β’ (π§ = β¨π, π¦β© β (πβπ§) = (πββ¨π, π¦β©)) |
54 | | df-ov 7364 |
. . . . . . 7
β’ (πππ¦) = (πββ¨π, π¦β©) |
55 | 53, 54 | eqtr4di 2791 |
. . . . . 6
β’ (π§ = β¨π, π¦β© β (πβπ§) = (πππ¦)) |
56 | | fveq2 6846 |
. . . . . . . 8
β’ (π§ = β¨π, π¦β© β ((1st βπ)βπ§) = ((1st βπ)ββ¨π, π¦β©)) |
57 | | df-ov 7364 |
. . . . . . . 8
β’ (π(1st βπ)π¦) = ((1st βπ)ββ¨π, π¦β©) |
58 | 56, 57 | eqtr4di 2791 |
. . . . . . 7
β’ (π§ = β¨π, π¦β© β ((1st βπ)βπ§) = (π(1st βπ)π¦)) |
59 | | fveq2 6846 |
. . . . . . . 8
β’ (π§ = β¨π, π¦β© β ((1st βπΈ)βπ§) = ((1st βπΈ)ββ¨π, π¦β©)) |
60 | | df-ov 7364 |
. . . . . . . 8
β’ (π(1st βπΈ)π¦) = ((1st βπΈ)ββ¨π, π¦β©) |
61 | 59, 60 | eqtr4di 2791 |
. . . . . . 7
β’ (π§ = β¨π, π¦β© β ((1st βπΈ)βπ§) = (π(1st βπΈ)π¦)) |
62 | 58, 61 | oveq12d 7379 |
. . . . . 6
β’ (π§ = β¨π, π¦β© β (((1st βπ)βπ§)(Hom βπ)((1st βπΈ)βπ§)) = ((π(1st βπ)π¦)(Hom βπ)(π(1st βπΈ)π¦))) |
63 | 55, 62 | eleq12d 2828 |
. . . . 5
β’ (π§ = β¨π, π¦β© β ((πβπ§) β (((1st βπ)βπ§)(Hom βπ)((1st βπΈ)βπ§)) β (πππ¦) β ((π(1st βπ)π¦)(Hom βπ)(π(1st βπΈ)π¦)))) |
64 | 63 | ralxp 5801 |
. . . 4
β’
(βπ§ β
((π Func π) Γ π΅)(πβπ§) β (((1st βπ)βπ§)(Hom βπ)((1st βπΈ)βπ§)) β βπ β (π Func π)βπ¦ β π΅ (πππ¦) β ((π(1st βπ)π¦)(Hom βπ)(π(1st βπΈ)π¦))) |
65 | 52, 64 | sylibr 233 |
. . 3
β’ (π β βπ§ β ((π Func π) Γ π΅)(πβπ§) β (((1st βπ)βπ§)(Hom βπ)((1st βπΈ)βπ§))) |
66 | | ovex 7394 |
. . . . . 6
β’ (π Func π) β V |
67 | 7 | fvexi 6860 |
. . . . . 6
β’ π΅ β V |
68 | 66, 67 | mpoex 8016 |
. . . . 5
β’ (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) β V |
69 | 1, 68 | eqeltri 2830 |
. . . 4
β’ π β V |
70 | 69 | elixp 8848 |
. . 3
β’ (π β Xπ§ β
((π Func π) Γ π΅)(((1st βπ)βπ§)(Hom βπ)((1st βπΈ)βπ§)) β (π Fn ((π Func π) Γ π΅) β§ βπ§ β ((π Func π) Γ π΅)(πβπ§) β (((1st βπ)βπ§)(Hom βπ)((1st βπΈ)βπ§)))) |
71 | 5, 65, 70 | sylanbrc 584 |
. 2
β’ (π β π β Xπ§ β ((π Func π) Γ π΅)(((1st βπ)βπ§)(Hom βπ)((1st βπΈ)βπ§))) |
72 | 17 | adantr 482 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β πΆ β Cat) |
73 | 19 | adantr 482 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β π β π) |
74 | 21 | adantr 482 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ran (Homf
βπΆ) β π) |
75 | 23 | adantr 482 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (ran (Homf
βπ) βͺ π) β π) |
76 | | simpr1 1195 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β π§ β ((π Func π) Γ π΅)) |
77 | | xp1st 7957 |
. . . . . 6
β’ (π§ β ((π Func π) Γ π΅) β (1st βπ§) β (π Func π)) |
78 | 76, 77 | syl 17 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (1st βπ§) β (π Func π)) |
79 | | xp2nd 7958 |
. . . . . 6
β’ (π§ β ((π Func π) Γ π΅) β (2nd βπ§) β π΅) |
80 | 76, 79 | syl 17 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (2nd βπ§) β π΅) |
81 | | simpr2 1196 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β π€ β ((π Func π) Γ π΅)) |
82 | | xp1st 7957 |
. . . . . 6
β’ (π€ β ((π Func π) Γ π΅) β (1st βπ€) β (π Func π)) |
83 | 81, 82 | syl 17 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (1st βπ€) β (π Func π)) |
84 | | xp2nd 7958 |
. . . . . 6
β’ (π€ β ((π Func π) Γ π΅) β (2nd βπ€) β π΅) |
85 | 81, 84 | syl 17 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (2nd βπ€) β π΅) |
86 | | simpr3 1197 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β π β (π§(Hom β(π Γc π))π€)) |
87 | | eqid 2733 |
. . . . . . . . . 10
β’ (π Nat π) = (π Nat π) |
88 | 12, 87 | fuchom 17857 |
. . . . . . . . 9
β’ (π Nat π) = (Hom βπ) |
89 | | eqid 2733 |
. . . . . . . . 9
β’ (Hom
βπ) = (Hom
βπ) |
90 | | eqid 2733 |
. . . . . . . . 9
β’ (Hom
β(π
Γc π)) = (Hom β(π Γc π)) |
91 | 30, 33, 88, 89, 90, 76, 81 | xpchom 18076 |
. . . . . . . 8
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (π§(Hom β(π Γc π))π€) = (((1st βπ§)(π Nat π)(1st βπ€)) Γ ((2nd βπ§)(Hom βπ)(2nd βπ€)))) |
92 | | eqid 2733 |
. . . . . . . . . 10
β’ (Hom
βπΆ) = (Hom
βπΆ) |
93 | 92, 9 | oppchom 17604 |
. . . . . . . . 9
β’
((2nd βπ§)(Hom βπ)(2nd βπ€)) = ((2nd βπ€)(Hom βπΆ)(2nd βπ§)) |
94 | 93 | xpeq2i 5664 |
. . . . . . . 8
β’
(((1st βπ§)(π Nat π)(1st βπ€)) Γ ((2nd βπ§)(Hom βπ)(2nd βπ€))) = (((1st βπ§)(π Nat π)(1st βπ€)) Γ ((2nd βπ€)(Hom βπΆ)(2nd βπ§))) |
95 | 91, 94 | eqtrdi 2789 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (π§(Hom β(π Γc π))π€) = (((1st βπ§)(π Nat π)(1st βπ€)) Γ ((2nd βπ€)(Hom βπΆ)(2nd βπ§)))) |
96 | 86, 95 | eleqtrd 2836 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β π β (((1st βπ§)(π Nat π)(1st βπ€)) Γ ((2nd βπ€)(Hom βπΆ)(2nd βπ§)))) |
97 | | xp1st 7957 |
. . . . . 6
β’ (π β (((1st
βπ§)(π Nat π)(1st βπ€)) Γ ((2nd βπ€)(Hom βπΆ)(2nd βπ§))) β (1st βπ) β ((1st
βπ§)(π Nat π)(1st βπ€))) |
98 | 96, 97 | syl 17 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (1st βπ) β ((1st
βπ§)(π Nat π)(1st βπ€))) |
99 | | xp2nd 7958 |
. . . . . 6
β’ (π β (((1st
βπ§)(π Nat π)(1st βπ€)) Γ ((2nd βπ€)(Hom βπΆ)(2nd βπ§))) β (2nd βπ) β ((2nd
βπ€)(Hom βπΆ)(2nd βπ§))) |
100 | 96, 99 | syl 17 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (2nd βπ) β ((2nd
βπ€)(Hom βπΆ)(2nd βπ§))) |
101 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 72, 73, 74, 75, 78, 80, 83, 85, 98, 100, 1 | yonedalem3b 18176 |
. . . 4
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (((1st βπ€)π(2nd βπ€))(β¨((1st βπ§)(1st βπ)(2nd βπ§)), ((1st
βπ€)(1st
βπ)(2nd
βπ€))β©(compβπ)((1st βπ€)(1st βπΈ)(2nd βπ€)))((1st βπ)(β¨(1st βπ§), (2nd βπ§)β©(2nd
βπ)β¨(1st βπ€), (2nd βπ€)β©)(2nd
βπ))) =
(((1st βπ)(β¨(1st βπ§), (2nd βπ§)β©(2nd
βπΈ)β¨(1st βπ€), (2nd βπ€)β©)(2nd
βπ))(β¨((1st βπ§)(1st βπ)(2nd βπ§)), ((1st
βπ§)(1st
βπΈ)(2nd
βπ§))β©(compβπ)((1st βπ€)(1st βπΈ)(2nd βπ€)))((1st βπ§)π(2nd βπ§)))) |
102 | | 1st2nd2 7964 |
. . . . . . . . . 10
β’ (π§ β ((π Func π) Γ π΅) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
103 | 76, 102 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
104 | 103 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((1st βπ)βπ§) = ((1st βπ)ββ¨(1st βπ§), (2nd βπ§)β©)) |
105 | | df-ov 7364 |
. . . . . . . 8
β’
((1st βπ§)(1st βπ)(2nd βπ§)) = ((1st βπ)ββ¨(1st
βπ§), (2nd
βπ§)β©) |
106 | 104, 105 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((1st βπ)βπ§) = ((1st βπ§)(1st βπ)(2nd βπ§))) |
107 | | 1st2nd2 7964 |
. . . . . . . . . 10
β’ (π€ β ((π Func π) Γ π΅) β π€ = β¨(1st βπ€), (2nd βπ€)β©) |
108 | 81, 107 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β π€ = β¨(1st βπ€), (2nd βπ€)β©) |
109 | 108 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((1st βπ)βπ€) = ((1st βπ)ββ¨(1st βπ€), (2nd βπ€)β©)) |
110 | | df-ov 7364 |
. . . . . . . 8
β’
((1st βπ€)(1st βπ)(2nd βπ€)) = ((1st βπ)ββ¨(1st
βπ€), (2nd
βπ€)β©) |
111 | 109, 110 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((1st βπ)βπ€) = ((1st βπ€)(1st βπ)(2nd βπ€))) |
112 | 106, 111 | opeq12d 4842 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β β¨((1st
βπ)βπ§), ((1st βπ)βπ€)β© = β¨((1st βπ§)(1st βπ)(2nd βπ§)), ((1st
βπ€)(1st
βπ)(2nd
βπ€))β©) |
113 | 108 | fveq2d 6850 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((1st βπΈ)βπ€) = ((1st βπΈ)ββ¨(1st βπ€), (2nd βπ€)β©)) |
114 | | df-ov 7364 |
. . . . . . 7
β’
((1st βπ€)(1st βπΈ)(2nd βπ€)) = ((1st βπΈ)ββ¨(1st
βπ€), (2nd
βπ€)β©) |
115 | 113, 114 | eqtr4di 2791 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((1st βπΈ)βπ€) = ((1st βπ€)(1st βπΈ)(2nd βπ€))) |
116 | 112, 115 | oveq12d 7379 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (β¨((1st
βπ)βπ§), ((1st βπ)βπ€)β©(compβπ)((1st βπΈ)βπ€)) = (β¨((1st βπ§)(1st βπ)(2nd βπ§)), ((1st
βπ€)(1st
βπ)(2nd
βπ€))β©(compβπ)((1st βπ€)(1st βπΈ)(2nd βπ€)))) |
117 | 108 | fveq2d 6850 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (πβπ€) = (πββ¨(1st βπ€), (2nd βπ€)β©)) |
118 | | df-ov 7364 |
. . . . . 6
β’
((1st βπ€)π(2nd βπ€)) = (πββ¨(1st βπ€), (2nd βπ€)β©) |
119 | 117, 118 | eqtr4di 2791 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (πβπ€) = ((1st βπ€)π(2nd βπ€))) |
120 | 103, 108 | oveq12d 7379 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (π§(2nd βπ)π€) = (β¨(1st βπ§), (2nd βπ§)β©(2nd
βπ)β¨(1st βπ€), (2nd βπ€)β©)) |
121 | | 1st2nd2 7964 |
. . . . . . . 8
β’ (π β (((1st
βπ§)(π Nat π)(1st βπ€)) Γ ((2nd βπ€)(Hom βπΆ)(2nd βπ§))) β π = β¨(1st βπ), (2nd βπ)β©) |
122 | 96, 121 | syl 17 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β π = β¨(1st βπ), (2nd βπ)β©) |
123 | 120, 122 | fveq12d 6853 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((π§(2nd βπ)π€)βπ) = ((β¨(1st βπ§), (2nd βπ§)β©(2nd
βπ)β¨(1st βπ€), (2nd βπ€)β©)ββ¨(1st
βπ), (2nd
βπ)β©)) |
124 | | df-ov 7364 |
. . . . . 6
β’
((1st βπ)(β¨(1st βπ§), (2nd βπ§)β©(2nd
βπ)β¨(1st βπ€), (2nd βπ€)β©)(2nd
βπ)) =
((β¨(1st βπ§), (2nd βπ§)β©(2nd βπ)β¨(1st
βπ€), (2nd
βπ€)β©)ββ¨(1st
βπ), (2nd
βπ)β©) |
125 | 123, 124 | eqtr4di 2791 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((π§(2nd βπ)π€)βπ) = ((1st βπ)(β¨(1st
βπ§), (2nd
βπ§)β©(2nd βπ)β¨(1st
βπ€), (2nd
βπ€)β©)(2nd βπ))) |
126 | 116, 119,
125 | oveq123d 7382 |
. . . 4
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((πβπ€)(β¨((1st βπ)βπ§), ((1st βπ)βπ€)β©(compβπ)((1st βπΈ)βπ€))((π§(2nd βπ)π€)βπ)) = (((1st βπ€)π(2nd βπ€))(β¨((1st βπ§)(1st βπ)(2nd βπ§)), ((1st
βπ€)(1st
βπ)(2nd
βπ€))β©(compβπ)((1st βπ€)(1st βπΈ)(2nd βπ€)))((1st βπ)(β¨(1st βπ§), (2nd βπ§)β©(2nd
βπ)β¨(1st βπ€), (2nd βπ€)β©)(2nd
βπ)))) |
127 | 103 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((1st βπΈ)βπ§) = ((1st βπΈ)ββ¨(1st βπ§), (2nd βπ§)β©)) |
128 | | df-ov 7364 |
. . . . . . . 8
β’
((1st βπ§)(1st βπΈ)(2nd βπ§)) = ((1st βπΈ)ββ¨(1st
βπ§), (2nd
βπ§)β©) |
129 | 127, 128 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((1st βπΈ)βπ§) = ((1st βπ§)(1st βπΈ)(2nd βπ§))) |
130 | 106, 129 | opeq12d 4842 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β β¨((1st
βπ)βπ§), ((1st βπΈ)βπ§)β© = β¨((1st βπ§)(1st βπ)(2nd βπ§)), ((1st
βπ§)(1st
βπΈ)(2nd
βπ§))β©) |
131 | 130, 115 | oveq12d 7379 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (β¨((1st
βπ)βπ§), ((1st βπΈ)βπ§)β©(compβπ)((1st βπΈ)βπ€)) = (β¨((1st βπ§)(1st βπ)(2nd βπ§)), ((1st
βπ§)(1st
βπΈ)(2nd
βπ§))β©(compβπ)((1st βπ€)(1st βπΈ)(2nd βπ€)))) |
132 | 103, 108 | oveq12d 7379 |
. . . . . . 7
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (π§(2nd βπΈ)π€) = (β¨(1st βπ§), (2nd βπ§)β©(2nd
βπΈ)β¨(1st βπ€), (2nd βπ€)β©)) |
133 | 132, 122 | fveq12d 6853 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((π§(2nd βπΈ)π€)βπ) = ((β¨(1st βπ§), (2nd βπ§)β©(2nd
βπΈ)β¨(1st βπ€), (2nd βπ€)β©)ββ¨(1st
βπ), (2nd
βπ)β©)) |
134 | | df-ov 7364 |
. . . . . 6
β’
((1st βπ)(β¨(1st βπ§), (2nd βπ§)β©(2nd
βπΈ)β¨(1st βπ€), (2nd βπ€)β©)(2nd
βπ)) =
((β¨(1st βπ§), (2nd βπ§)β©(2nd βπΈ)β¨(1st
βπ€), (2nd
βπ€)β©)ββ¨(1st
βπ), (2nd
βπ)β©) |
135 | 133, 134 | eqtr4di 2791 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((π§(2nd βπΈ)π€)βπ) = ((1st βπ)(β¨(1st
βπ§), (2nd
βπ§)β©(2nd βπΈ)β¨(1st
βπ€), (2nd
βπ€)β©)(2nd βπ))) |
136 | 103 | fveq2d 6850 |
. . . . . 6
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (πβπ§) = (πββ¨(1st βπ§), (2nd βπ§)β©)) |
137 | | df-ov 7364 |
. . . . . 6
β’
((1st βπ§)π(2nd βπ§)) = (πββ¨(1st βπ§), (2nd βπ§)β©) |
138 | 136, 137 | eqtr4di 2791 |
. . . . 5
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (πβπ§) = ((1st βπ§)π(2nd βπ§))) |
139 | 131, 135,
138 | oveq123d 7382 |
. . . 4
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β (((π§(2nd βπΈ)π€)βπ)(β¨((1st βπ)βπ§), ((1st βπΈ)βπ§)β©(compβπ)((1st βπΈ)βπ€))(πβπ§)) = (((1st βπ)(β¨(1st
βπ§), (2nd
βπ§)β©(2nd βπΈ)β¨(1st
βπ€), (2nd
βπ€)β©)(2nd βπ))(β¨((1st
βπ§)(1st
βπ)(2nd
βπ§)),
((1st βπ§)(1st βπΈ)(2nd βπ§))β©(compβπ)((1st βπ€)(1st βπΈ)(2nd βπ€)))((1st βπ§)π(2nd βπ§)))) |
140 | 101, 126,
139 | 3eqtr4d 2783 |
. . 3
β’ ((π β§ (π§ β ((π Func π) Γ π΅) β§ π€ β ((π Func π) Γ π΅) β§ π β (π§(Hom β(π Γc π))π€))) β ((πβπ€)(β¨((1st βπ)βπ§), ((1st βπ)βπ€)β©(compβπ)((1st βπΈ)βπ€))((π§(2nd βπ)π€)βπ)) = (((π§(2nd βπΈ)π€)βπ)(β¨((1st βπ)βπ§), ((1st βπΈ)βπ§)β©(compβπ)((1st βπΈ)βπ€))(πβπ§))) |
141 | 140 | ralrimivvva 3197 |
. 2
β’ (π β βπ§ β ((π Func π) Γ π΅)βπ€ β ((π Func π) Γ π΅)βπ β (π§(Hom β(π Γc π))π€)((πβπ€)(β¨((1st βπ)βπ§), ((1st βπ)βπ€)β©(compβπ)((1st βπΈ)βπ€))((π§(2nd βπ)π€)βπ)) = (((π§(2nd βπΈ)π€)βπ)(β¨((1st βπ)βπ§), ((1st βπΈ)βπ§)β©(compβπ)((1st βπΈ)βπ€))(πβπ§))) |
142 | | eqid 2733 |
. . 3
β’ ((π Γc
π) Nat π) = ((π Γc π) Nat π) |
143 | | eqid 2733 |
. . 3
β’
(compβπ) =
(compβπ) |
144 | 142, 33, 90, 29, 143, 37, 44 | isnat2 17843 |
. 2
β’ (π β (π β (π((π Γc π) Nat π)πΈ) β (π β Xπ§ β ((π Func π) Γ π΅)(((1st βπ)βπ§)(Hom βπ)((1st βπΈ)βπ§)) β§ βπ§ β ((π Func π) Γ π΅)βπ€ β ((π Func π) Γ π΅)βπ β (π§(Hom β(π Γc π))π€)((πβπ€)(β¨((1st βπ)βπ§), ((1st βπ)βπ€)β©(compβπ)((1st βπΈ)βπ€))((π§(2nd βπ)π€)βπ)) = (((π§(2nd βπΈ)π€)βπ)(β¨((1st βπ)βπ§), ((1st βπΈ)βπ§)β©(compβπ)((1st βπΈ)βπ€))(πβπ§))))) |
145 | 71, 141, 144 | mpbir2and 712 |
1
β’ (π β π β (π((π Γc π) Nat π)πΈ)) |