Step | Hyp | Ref
| Expression |
1 | | invfuc.u |
. 2
β’ (π β π β (πΉππΊ)) |
2 | | invfuc.v |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))π) |
3 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ·) =
(Baseβπ·) |
4 | | fucinv.j |
. . . . . . . . . 10
β’ π½ = (Invβπ·) |
5 | | fuciso.f |
. . . . . . . . . . . . 13
β’ (π β πΉ β (πΆ Func π·)) |
6 | | funcrcl 17754 |
. . . . . . . . . . . . 13
β’ (πΉ β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (πΆ β Cat β§ π· β Cat)) |
8 | 7 | simprd 497 |
. . . . . . . . . . 11
β’ (π β π· β Cat) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β π· β Cat) |
10 | | fuciso.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΆ) |
11 | | relfunc 17753 |
. . . . . . . . . . . . 13
β’ Rel
(πΆ Func π·) |
12 | | 1st2ndbr 7975 |
. . . . . . . . . . . . 13
β’ ((Rel
(πΆ Func π·) β§ πΉ β (πΆ Func π·)) β (1st βπΉ)(πΆ Func π·)(2nd βπΉ)) |
13 | 11, 5, 12 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (1st
βπΉ)(πΆ Func π·)(2nd βπΉ)) |
14 | 10, 3, 13 | funcf1 17757 |
. . . . . . . . . . 11
β’ (π β (1st
βπΉ):π΅βΆ(Baseβπ·)) |
15 | 14 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β ((1st βπΉ)βπ₯) β (Baseβπ·)) |
16 | | fuciso.g |
. . . . . . . . . . . . 13
β’ (π β πΊ β (πΆ Func π·)) |
17 | | 1st2ndbr 7975 |
. . . . . . . . . . . . 13
β’ ((Rel
(πΆ Func π·) β§ πΊ β (πΆ Func π·)) β (1st βπΊ)(πΆ Func π·)(2nd βπΊ)) |
18 | 11, 16, 17 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (1st
βπΊ)(πΆ Func π·)(2nd βπΊ)) |
19 | 10, 3, 18 | funcf1 17757 |
. . . . . . . . . . 11
β’ (π β (1st
βπΊ):π΅βΆ(Baseβπ·)) |
20 | 19 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β ((1st βπΊ)βπ₯) β (Baseβπ·)) |
21 | | eqid 2733 |
. . . . . . . . . 10
β’ (Hom
βπ·) = (Hom
βπ·) |
22 | 3, 4, 9, 15, 20, 21 | invss 17649 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)) β ((((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΊ)βπ₯)) Γ (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)))) |
23 | 22 | ssbrd 5149 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β ((πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))π β (πβπ₯)((((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΊ)βπ₯)) Γ (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)))π)) |
24 | 2, 23 | mpd 15 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β (πβπ₯)((((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΊ)βπ₯)) Γ (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)))π) |
25 | | brxp 5682 |
. . . . . . . 8
β’ ((πβπ₯)((((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΊ)βπ₯)) Γ (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)))π β ((πβπ₯) β (((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΊ)βπ₯)) β§ π β (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)))) |
26 | 25 | simprbi 498 |
. . . . . . 7
β’ ((πβπ₯)((((1st βπΉ)βπ₯)(Hom βπ·)((1st βπΊ)βπ₯)) Γ (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)))π β π β (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯))) |
27 | 24, 26 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β π β (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯))) |
28 | 27 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ₯ β π΅ π β (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯))) |
29 | 10 | fvexi 6857 |
. . . . . 6
β’ π΅ β V |
30 | | mptelixpg 8876 |
. . . . . 6
β’ (π΅ β V β ((π₯ β π΅ β¦ π) β Xπ₯ β π΅ (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)) β βπ₯ β π΅ π β (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)))) |
31 | 29, 30 | ax-mp 5 |
. . . . 5
β’ ((π₯ β π΅ β¦ π) β Xπ₯ β π΅ (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)) β βπ₯ β π΅ π β (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯))) |
32 | 28, 31 | sylibr 233 |
. . . 4
β’ (π β (π₯ β π΅ β¦ π) β Xπ₯ β π΅ (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯))) |
33 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = π¦ β ((1st βπΊ)βπ₯) = ((1st βπΊ)βπ¦)) |
34 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = π¦ β ((1st βπΉ)βπ₯) = ((1st βπΉ)βπ¦)) |
35 | 33, 34 | oveq12d 7376 |
. . . . 5
β’ (π₯ = π¦ β (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)) = (((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΉ)βπ¦))) |
36 | 35 | cbvixpv 8856 |
. . . 4
β’ Xπ₯ β
π΅ (((1st
βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯)) = Xπ¦ β π΅ (((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΉ)βπ¦)) |
37 | 32, 36 | eleqtrdi 2844 |
. . 3
β’ (π β (π₯ β π΅ β¦ π) β Xπ¦ β π΅ (((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΉ)βπ¦))) |
38 | | simpr2 1196 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β π§ β π΅) |
39 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β π΅) β π₯ β π΅) |
40 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π΅ β¦ π) = (π₯ β π΅ β¦ π) |
41 | 40 | fvmpt2 6960 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β π΅ β§ π β (((1st βπΊ)βπ₯)(Hom βπ·)((1st βπΉ)βπ₯))) β ((π₯ β π΅ β¦ π)βπ₯) = π) |
42 | 39, 27, 41 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β π΅) β ((π₯ β π΅ β¦ π)βπ₯) = π) |
43 | 2, 42 | breqtrrd 5134 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΅) β (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯)) |
44 | 43 | ralrimiva 3140 |
. . . . . . . . . . . . . . 15
β’ (π β βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯)) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯)) |
46 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²π₯(πβπ§) |
47 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²π₯(((1st βπΉ)βπ§)π½((1st βπΊ)βπ§)) |
48 | | nffvmpt1 6854 |
. . . . . . . . . . . . . . . 16
β’
β²π₯((π₯ β π΅ β¦ π)βπ§) |
49 | 46, 47, 48 | nfbr 5153 |
. . . . . . . . . . . . . . 15
β’
β²π₯(πβπ§)(((1st βπΉ)βπ§)π½((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§) |
50 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β (πβπ₯) = (πβπ§)) |
51 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β ((1st βπΉ)βπ₯) = ((1st βπΉ)βπ§)) |
52 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β ((1st βπΊ)βπ₯) = ((1st βπΊ)βπ§)) |
53 | 51, 52 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)) = (((1st βπΉ)βπ§)π½((1st βπΊ)βπ§))) |
54 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β ((π₯ β π΅ β¦ π)βπ₯) = ((π₯ β π΅ β¦ π)βπ§)) |
55 | 50, 53, 54 | breq123d 5120 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β ((πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯) β (πβπ§)(((1st βπΉ)βπ§)π½((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§))) |
56 | 49, 55 | rspc 3568 |
. . . . . . . . . . . . . 14
β’ (π§ β π΅ β (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯) β (πβπ§)(((1st βπΉ)βπ§)π½((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§))) |
57 | 38, 45, 56 | sylc 65 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (πβπ§)(((1st βπΉ)βπ§)π½((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§)) |
58 | 8 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β π· β Cat) |
59 | 14 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (1st βπΉ):π΅βΆ(Baseβπ·)) |
60 | 59, 38 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((1st βπΉ)βπ§) β (Baseβπ·)) |
61 | 19 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (1st βπΊ):π΅βΆ(Baseβπ·)) |
62 | 61, 38 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((1st βπΊ)βπ§) β (Baseβπ·)) |
63 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Sectβπ·) =
(Sectβπ·) |
64 | 3, 4, 58, 60, 62, 63 | isinv 17648 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((πβπ§)(((1st βπΉ)βπ§)π½((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§) β ((πβπ§)(((1st βπΉ)βπ§)(Sectβπ·)((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§) β§ ((π₯ β π΅ β¦ π)βπ§)(((1st βπΊ)βπ§)(Sectβπ·)((1st βπΉ)βπ§))(πβπ§)))) |
65 | 57, 64 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((πβπ§)(((1st βπΉ)βπ§)(Sectβπ·)((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§) β§ ((π₯ β π΅ β¦ π)βπ§)(((1st βπΊ)βπ§)(Sectβπ·)((1st βπΉ)βπ§))(πβπ§))) |
66 | 65 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (πβπ§)(((1st βπΉ)βπ§)(Sectβπ·)((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§)) |
67 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(compβπ·) =
(compβπ·) |
68 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Idβπ·) =
(Idβπ·) |
69 | 3, 21, 67, 68, 63, 58, 60, 62 | issect 17641 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((πβπ§)(((1st βπΉ)βπ§)(Sectβπ·)((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ§) β ((πβπ§) β (((1st βπΉ)βπ§)(Hom βπ·)((1st βπΊ)βπ§)) β§ ((π₯ β π΅ β¦ π)βπ§) β (((1st βπΊ)βπ§)(Hom βπ·)((1st βπΉ)βπ§)) β§ (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ§), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(πβπ§)) = ((Idβπ·)β((1st βπΉ)βπ§))))) |
70 | 66, 69 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((πβπ§) β (((1st βπΉ)βπ§)(Hom βπ·)((1st βπΊ)βπ§)) β§ ((π₯ β π΅ β¦ π)βπ§) β (((1st βπΊ)βπ§)(Hom βπ·)((1st βπΉ)βπ§)) β§ (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ§), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(πβπ§)) = ((Idβπ·)β((1st βπΉ)βπ§)))) |
71 | 70 | simp3d 1145 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ§), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(πβπ§)) = ((Idβπ·)β((1st βπΉ)βπ§))) |
72 | 71 | oveq1d 7373 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ§), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(πβπ§))(β¨((1st βπΉ)βπ¦), ((1st βπΉ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΉ)π§)βπ)) = (((Idβπ·)β((1st βπΉ)βπ§))(β¨((1st βπΉ)βπ¦), ((1st βπΉ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΉ)π§)βπ))) |
73 | | simpr1 1195 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β π¦ β π΅) |
74 | 59, 73 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((1st βπΉ)βπ¦) β (Baseβπ·)) |
75 | | eqid 2733 |
. . . . . . . . . . 11
β’ (Hom
βπΆ) = (Hom
βπΆ) |
76 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (1st βπΉ)(πΆ Func π·)(2nd βπΉ)) |
77 | 10, 75, 21, 76, 73, 38 | funcf2 17759 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (π¦(2nd βπΉ)π§):(π¦(Hom βπΆ)π§)βΆ(((1st βπΉ)βπ¦)(Hom βπ·)((1st βπΉ)βπ§))) |
78 | | simpr3 1197 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β π β (π¦(Hom βπΆ)π§)) |
79 | 77, 78 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((π¦(2nd βπΉ)π§)βπ) β (((1st βπΉ)βπ¦)(Hom βπ·)((1st βπΉ)βπ§))) |
80 | 3, 21, 68, 58, 74, 67, 60, 79 | catlid 17568 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((Idβπ·)β((1st βπΉ)βπ§))(β¨((1st βπΉ)βπ¦), ((1st βπΉ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΉ)π§)βπ)) = ((π¦(2nd βπΉ)π§)βπ)) |
81 | 72, 80 | eqtr2d 2774 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((π¦(2nd βπΉ)π§)βπ) = ((((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ§), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(πβπ§))(β¨((1st βπΉ)βπ¦), ((1st βπΉ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΉ)π§)βπ))) |
82 | | fuciso.n |
. . . . . . . . 9
β’ π = (πΆ Nat π·) |
83 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β π β (πΉππΊ)) |
84 | 82, 83 | nat1st2nd 17843 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β π β (β¨(1st βπΉ), (2nd βπΉ)β©πβ¨(1st βπΊ), (2nd βπΊ)β©)) |
85 | 82, 84, 10, 21, 38 | natcl 17845 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (πβπ§) β (((1st βπΉ)βπ§)(Hom βπ·)((1st βπΊ)βπ§))) |
86 | 70 | simp2d 1144 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((π₯ β π΅ β¦ π)βπ§) β (((1st βπΊ)βπ§)(Hom βπ·)((1st βπΉ)βπ§))) |
87 | 3, 21, 67, 58, 74, 60, 62, 79, 85, 60, 86 | catass 17571 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ§), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(πβπ§))(β¨((1st βπΉ)βπ¦), ((1st βπΉ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΉ)π§)βπ)) = (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((πβπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΉ)βπ§)β©(compβπ·)((1st βπΊ)βπ§))((π¦(2nd βπΉ)π§)βπ)))) |
88 | 82, 84, 10, 75, 67, 73, 38, 78 | nati 17847 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((πβπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΉ)βπ§)β©(compβπ·)((1st βπΊ)βπ§))((π¦(2nd βπΉ)π§)βπ)) = (((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦))) |
89 | 88 | oveq2d 7374 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((πβπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΉ)βπ§)β©(compβπ·)((1st βπΊ)βπ§))((π¦(2nd βπΉ)π§)βπ))) = (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦)))) |
90 | 81, 87, 89 | 3eqtrd 2777 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((π¦(2nd βπΉ)π§)βπ) = (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦)))) |
91 | 90 | oveq1d 7373 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π¦(2nd βπΉ)π§)βπ)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯ β π΅ β¦ π)βπ¦)) = ((((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦)))(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯ β π΅ β¦ π)βπ¦))) |
92 | 61, 73 | ffvelcdmd 7037 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((1st βπΊ)βπ¦) β (Baseβπ·)) |
93 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯(πβπ¦) |
94 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦)) |
95 | | nffvmpt1 6854 |
. . . . . . . . . . . . 13
β’
β²π₯((π₯ β π΅ β¦ π)βπ¦) |
96 | 93, 94, 95 | nfbr 5153 |
. . . . . . . . . . . 12
β’
β²π₯(πβπ¦)(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦) |
97 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (πβπ₯) = (πβπ¦)) |
98 | 34, 33 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)) = (((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))) |
99 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β ((π₯ β π΅ β¦ π)βπ₯) = ((π₯ β π΅ β¦ π)βπ¦)) |
100 | 97, 98, 99 | breq123d 5120 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β ((πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯) β (πβπ¦)(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦))) |
101 | 96, 100 | rspc 3568 |
. . . . . . . . . . 11
β’ (π¦ β π΅ β (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯) β (πβπ¦)(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦))) |
102 | 73, 45, 101 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (πβπ¦)(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦)) |
103 | 3, 4, 58, 74, 92, 63 | isinv 17648 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((πβπ¦)(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦) β ((πβπ¦)(((1st βπΉ)βπ¦)(Sectβπ·)((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦) β§ ((π₯ β π΅ β¦ π)βπ¦)(((1st βπΊ)βπ¦)(Sectβπ·)((1st βπΉ)βπ¦))(πβπ¦)))) |
104 | 102, 103 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((πβπ¦)(((1st βπΉ)βπ¦)(Sectβπ·)((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦) β§ ((π₯ β π΅ β¦ π)βπ¦)(((1st βπΊ)βπ¦)(Sectβπ·)((1st βπΉ)βπ¦))(πβπ¦))) |
105 | 104 | simprd 497 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((π₯ β π΅ β¦ π)βπ¦)(((1st βπΊ)βπ¦)(Sectβπ·)((1st βπΉ)βπ¦))(πβπ¦)) |
106 | 3, 21, 67, 68, 63, 58, 92, 74 | issect 17641 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π₯ β π΅ β¦ π)βπ¦)(((1st βπΊ)βπ¦)(Sectβπ·)((1st βπΉ)βπ¦))(πβπ¦) β (((π₯ β π΅ β¦ π)βπ¦) β (((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΉ)βπ¦)) β§ (πβπ¦) β (((1st βπΉ)βπ¦)(Hom βπ·)((1st βπΊ)βπ¦)) β§ ((πβπ¦)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦)) = ((Idβπ·)β((1st βπΊ)βπ¦))))) |
107 | 105, 106 | mpbid 231 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π₯ β π΅ β¦ π)βπ¦) β (((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΉ)βπ¦)) β§ (πβπ¦) β (((1st βπΉ)βπ¦)(Hom βπ·)((1st βπΊ)βπ¦)) β§ ((πβπ¦)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦)) = ((Idβπ·)β((1st βπΊ)βπ¦)))) |
108 | 107 | simp1d 1143 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((π₯ β π΅ β¦ π)βπ¦) β (((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΉ)βπ¦))) |
109 | 107 | simp2d 1144 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (πβπ¦) β (((1st βπΉ)βπ¦)(Hom βπ·)((1st βπΊ)βπ¦))) |
110 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (1st βπΊ)(πΆ Func π·)(2nd βπΊ)) |
111 | 10, 75, 21, 110, 73, 38 | funcf2 17759 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (π¦(2nd βπΊ)π§):(π¦(Hom βπΆ)π§)βΆ(((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΊ)βπ§))) |
112 | 111, 78 | ffvelcdmd 7037 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((π¦(2nd βπΊ)π§)βπ) β (((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΊ)βπ§))) |
113 | 3, 21, 67, 58, 74, 92, 62, 109, 112 | catcocl 17570 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦)) β (((1st βπΉ)βπ¦)(Hom βπ·)((1st βπΊ)βπ§))) |
114 | 3, 21, 67, 58, 92, 74, 62, 108, 113, 60, 86 | catass 17571 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))(((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦)))(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯ β π΅ β¦ π)βπ¦)) = (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦))(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ¦)))) |
115 | 82, 84, 10, 21, 73 | natcl 17845 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (πβπ¦) β (((1st βπΉ)βπ¦)(Hom βπ·)((1st βπΊ)βπ¦))) |
116 | 3, 21, 67, 58, 92, 74, 92, 108, 115, 62, 112 | catass 17571 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦))(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ¦)) = (((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))((πβπ¦)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦)))) |
117 | 107 | simp3d 1145 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((πβπ¦)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦)) = ((Idβπ·)β((1st βπΊ)βπ¦))) |
118 | 117 | oveq2d 7374 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))((πβπ¦)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦))) = (((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))((Idβπ·)β((1st βπΊ)βπ¦)))) |
119 | 3, 21, 68, 58, 92, 67, 62, 112 | catrid 17569 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))((Idβπ·)β((1st βπΊ)βπ¦))) = ((π¦(2nd βπΊ)π§)βπ)) |
120 | 116, 118,
119 | 3eqtrd 2777 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β ((((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦))(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ¦)) = ((π¦(2nd βπΊ)π§)βπ)) |
121 | 120 | oveq2d 7374 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((((π¦(2nd βπΊ)π§)βπ)(β¨((1st βπΉ)βπ¦), ((1st βπΊ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))(πβπ¦))(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΊ)βπ§))((π₯ β π΅ β¦ π)βπ¦))) = (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΊ)π§)βπ))) |
122 | 91, 114, 121 | 3eqtrrd 2778 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅ β§ π β (π¦(Hom βπΆ)π§))) β (((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΊ)π§)βπ)) = (((π¦(2nd βπΉ)π§)βπ)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯ β π΅ β¦ π)βπ¦))) |
123 | 122 | ralrimivvva 3197 |
. . 3
β’ (π β βπ¦ β π΅ βπ§ β π΅ βπ β (π¦(Hom βπΆ)π§)(((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΊ)π§)βπ)) = (((π¦(2nd βπΉ)π§)βπ)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯ β π΅ β¦ π)βπ¦))) |
124 | 82, 10, 75, 21, 67, 16, 5 | isnat2 17840 |
. . 3
β’ (π β ((π₯ β π΅ β¦ π) β (πΊππΉ) β ((π₯ β π΅ β¦ π) β Xπ¦ β π΅ (((1st βπΊ)βπ¦)(Hom βπ·)((1st βπΉ)βπ¦)) β§ βπ¦ β π΅ βπ§ β π΅ βπ β (π¦(Hom βπΆ)π§)(((π₯ β π΅ β¦ π)βπ§)(β¨((1st βπΊ)βπ¦), ((1st βπΊ)βπ§)β©(compβπ·)((1st βπΉ)βπ§))((π¦(2nd βπΊ)π§)βπ)) = (((π¦(2nd βπΉ)π§)βπ)(β¨((1st βπΊ)βπ¦), ((1st βπΉ)βπ¦)β©(compβπ·)((1st βπΉ)βπ§))((π₯ β π΅ β¦ π)βπ¦))))) |
125 | 37, 123, 124 | mpbir2and 712 |
. 2
β’ (π β (π₯ β π΅ β¦ π) β (πΊππΉ)) |
126 | | nfv 1918 |
. . . 4
β’
β²π¦(πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯) |
127 | 126, 96, 100 | cbvralw 3288 |
. . 3
β’
(βπ₯ β
π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))((π₯ β π΅ β¦ π)βπ₯) β βπ¦ β π΅ (πβπ¦)(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦)) |
128 | 44, 127 | sylib 217 |
. 2
β’ (π β βπ¦ β π΅ (πβπ¦)(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦)) |
129 | | fuciso.q |
. . 3
β’ π = (πΆ FuncCat π·) |
130 | | fucinv.i |
. . 3
β’ πΌ = (Invβπ) |
131 | 129, 10, 82, 5, 16, 130, 4 | fucinv 17867 |
. 2
β’ (π β (π(πΉπΌπΊ)(π₯ β π΅ β¦ π) β (π β (πΉππΊ) β§ (π₯ β π΅ β¦ π) β (πΊππΉ) β§ βπ¦ β π΅ (πβπ¦)(((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))((π₯ β π΅ β¦ π)βπ¦)))) |
132 | 1, 125, 128, 131 | mpbir3and 1343 |
1
β’ (π β π(πΉπΌπΊ)(π₯ β π΅ β¦ π)) |