Step | Hyp | Ref
| Expression |
1 | | relfunc 17683 |
. . . . 5
β’ Rel
(π Func π) |
2 | | catciso.b |
. . . . . . . . . . . . . 14
β’ π΅ = (BaseβπΆ) |
3 | | eqid 2738 |
. . . . . . . . . . . . . 14
β’
(InvβπΆ) =
(InvβπΆ) |
4 | | catciso.u |
. . . . . . . . . . . . . . 15
β’ (π β π β π) |
5 | | catciso.c |
. . . . . . . . . . . . . . . 16
β’ πΆ = (CatCatβπ) |
6 | 5 | catccat 17929 |
. . . . . . . . . . . . . . 15
β’ (π β π β πΆ β Cat) |
7 | 4, 6 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β Cat) |
8 | | catciso.x |
. . . . . . . . . . . . . 14
β’ (π β π β π΅) |
9 | | catciso.y |
. . . . . . . . . . . . . 14
β’ (π β π β π΅) |
10 | | catciso.i |
. . . . . . . . . . . . . 14
β’ πΌ = (IsoβπΆ) |
11 | 2, 3, 7, 8, 9, 10 | isoval 17583 |
. . . . . . . . . . . . 13
β’ (π β (ππΌπ) = dom (π(InvβπΆ)π)) |
12 | 11 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ (π β (πΉ β (ππΌπ) β πΉ β dom (π(InvβπΆ)π))) |
13 | 12 | biimpa 478 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΌπ)) β πΉ β dom (π(InvβπΆ)π)) |
14 | 7 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ β (ππΌπ)) β πΆ β Cat) |
15 | 8 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ β (ππΌπ)) β π β π΅) |
16 | 9 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ β (ππΌπ)) β π β π΅) |
17 | 2, 3, 14, 15, 16 | invfun 17582 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ β (ππΌπ)) β Fun (π(InvβπΆ)π)) |
18 | | funfvbrb 6997 |
. . . . . . . . . . . 12
β’ (Fun
(π(InvβπΆ)π) β (πΉ β dom (π(InvβπΆ)π) β πΉ(π(InvβπΆ)π)((π(InvβπΆ)π)βπΉ))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ β dom (π(InvβπΆ)π) β πΉ(π(InvβπΆ)π)((π(InvβπΆ)π)βπΉ))) |
20 | 13, 19 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΌπ)) β πΉ(π(InvβπΆ)π)((π(InvβπΆ)π)βπΉ)) |
21 | | eqid 2738 |
. . . . . . . . . . 11
β’
(SectβπΆ) =
(SectβπΆ) |
22 | 2, 3, 14, 15, 16, 21 | isinv 17578 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ(π(InvβπΆ)π)((π(InvβπΆ)π)βπΉ) β (πΉ(π(SectβπΆ)π)((π(InvβπΆ)π)βπΉ) β§ ((π(InvβπΆ)π)βπΉ)(π(SectβπΆ)π)πΉ))) |
23 | 20, 22 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ(π(SectβπΆ)π)((π(InvβπΆ)π)βπΉ) β§ ((π(InvβπΆ)π)βπΉ)(π(SectβπΆ)π)πΉ)) |
24 | 23 | simpld 496 |
. . . . . . . 8
β’ ((π β§ πΉ β (ππΌπ)) β πΉ(π(SectβπΆ)π)((π(InvβπΆ)π)βπΉ)) |
25 | | eqid 2738 |
. . . . . . . . 9
β’ (Hom
βπΆ) = (Hom
βπΆ) |
26 | | eqid 2738 |
. . . . . . . . 9
β’
(compβπΆ) =
(compβπΆ) |
27 | | eqid 2738 |
. . . . . . . . 9
β’
(IdβπΆ) =
(IdβπΆ) |
28 | 2, 25, 26, 27, 21, 14, 15, 16 | issect 17571 |
. . . . . . . 8
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ(π(SectβπΆ)π)((π(InvβπΆ)π)βπΉ) β (πΉ β (π(Hom βπΆ)π) β§ ((π(InvβπΆ)π)βπΉ) β (π(Hom βπΆ)π) β§ (((π(InvβπΆ)π)βπΉ)(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)))) |
29 | 24, 28 | mpbid 231 |
. . . . . . 7
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ β (π(Hom βπΆ)π) β§ ((π(InvβπΆ)π)βπΉ) β (π(Hom βπΆ)π) β§ (((π(InvβπΆ)π)βπΉ)(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ))) |
30 | 29 | simp1d 1143 |
. . . . . 6
β’ ((π β§ πΉ β (ππΌπ)) β πΉ β (π(Hom βπΆ)π)) |
31 | 5, 2, 4, 25, 8, 9 | catchom 17924 |
. . . . . . 7
β’ (π β (π(Hom βπΆ)π) = (π Func π)) |
32 | 31 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (ππΌπ)) β (π(Hom βπΆ)π) = (π Func π)) |
33 | 30, 32 | eleqtrd 2841 |
. . . . 5
β’ ((π β§ πΉ β (ππΌπ)) β πΉ β (π Func π)) |
34 | | 1st2nd 7961 |
. . . . 5
β’ ((Rel
(π Func π) β§ πΉ β (π Func π)) β πΉ = β¨(1st βπΉ), (2nd βπΉ)β©) |
35 | 1, 33, 34 | sylancr 588 |
. . . 4
β’ ((π β§ πΉ β (ππΌπ)) β πΉ = β¨(1st βπΉ), (2nd βπΉ)β©) |
36 | | 1st2ndbr 7964 |
. . . . . . 7
β’ ((Rel
(π Func π) β§ πΉ β (π Func π)) β (1st βπΉ)(π Func π)(2nd βπΉ)) |
37 | 1, 33, 36 | sylancr 588 |
. . . . . 6
β’ ((π β§ πΉ β (ππΌπ)) β (1st βπΉ)(π Func π)(2nd βπΉ)) |
38 | | catciso.r |
. . . . . . . . 9
β’ π
= (Baseβπ) |
39 | | eqid 2738 |
. . . . . . . . 9
β’ (Hom
βπ) = (Hom
βπ) |
40 | | eqid 2738 |
. . . . . . . . 9
β’ (Hom
βπ) = (Hom
βπ) |
41 | 37 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (1st βπΉ)(π Func π)(2nd βπΉ)) |
42 | | simprl 770 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β π₯ β π
) |
43 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β π¦ β π
) |
44 | 38, 39, 40, 41, 42, 43 | funcf2 17689 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (π₯(2nd βπΉ)π¦):(π₯(Hom βπ)π¦)βΆ(((1st βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦))) |
45 | | catciso.s |
. . . . . . . . . 10
β’ π = (Baseβπ) |
46 | | relfunc 17683 |
. . . . . . . . . . . 12
β’ Rel
(π Func π) |
47 | 29 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ β (ππΌπ)) β ((π(InvβπΆ)π)βπΉ) β (π(Hom βπΆ)π)) |
48 | 5, 2, 4, 25, 9, 8 | catchom 17924 |
. . . . . . . . . . . . . 14
β’ (π β (π(Hom βπΆ)π) = (π Func π)) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ β (ππΌπ)) β (π(Hom βπΆ)π) = (π Func π)) |
50 | 47, 49 | eleqtrd 2841 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ β (ππΌπ)) β ((π(InvβπΆ)π)βπΉ) β (π Func π)) |
51 | | 1st2ndbr 7964 |
. . . . . . . . . . . 12
β’ ((Rel
(π Func π) β§ ((π(InvβπΆ)π)βπΉ) β (π Func π)) β (1st β((π(InvβπΆ)π)βπΉ))(π Func π)(2nd β((π(InvβπΆ)π)βπΉ))) |
52 | 46, 50, 51 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΌπ)) β (1st β((π(InvβπΆ)π)βπΉ))(π Func π)(2nd β((π(InvβπΆ)π)βπΉ))) |
53 | 52 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (1st β((π(InvβπΆ)π)βπΉ))(π Func π)(2nd β((π(InvβπΆ)π)βπΉ))) |
54 | 38, 45, 41 | funcf1 17687 |
. . . . . . . . . . 11
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (1st βπΉ):π
βΆπ) |
55 | 54, 42 | ffvelcdmd 7031 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st βπΉ)βπ₯) β π) |
56 | 54, 43 | ffvelcdmd 7031 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st βπΉ)βπ¦) β π) |
57 | 45, 40, 39, 53, 55, 56 | funcf2 17689 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)):(((1st βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦))βΆ(((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ₯))(Hom βπ)((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ¦)))) |
58 | 29 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ πΉ β (ππΌπ)) β (((π(InvβπΆ)π)βπΉ)(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) |
59 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ πΉ β (ππΌπ)) β π β π) |
60 | 5, 2, 59, 26, 15, 16, 15, 33, 50 | catcco 17926 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ πΉ β (ππΌπ)) β (((π(InvβπΆ)π)βπΉ)(β¨π, πβ©(compβπΆ)π)πΉ) = (((π(InvβπΆ)π)βπΉ) βfunc πΉ)) |
61 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
β’
(idfuncβπ) = (idfuncβπ) |
62 | 5, 2, 27, 61, 4, 8 | catcid 17928 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((IdβπΆ)βπ) = (idfuncβπ)) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ πΉ β (ππΌπ)) β ((IdβπΆ)βπ) = (idfuncβπ)) |
64 | 58, 60, 63 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΉ β (ππΌπ)) β (((π(InvβπΆ)π)βπΉ) βfunc πΉ) =
(idfuncβπ)) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((π(InvβπΆ)π)βπΉ) βfunc πΉ) =
(idfuncβπ)) |
66 | 65 | fveq2d 6842 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (1st β(((π(InvβπΆ)π)βπΉ) βfunc πΉ)) = (1st
β(idfuncβπ))) |
67 | 66 | fveq1d 6840 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st β(((π(InvβπΆ)π)βπΉ) βfunc πΉ))βπ₯) = ((1st
β(idfuncβπ))βπ₯)) |
68 | 33 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β πΉ β (π Func π)) |
69 | 50 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((π(InvβπΆ)π)βπΉ) β (π Func π)) |
70 | 38, 68, 69, 42 | cofu1 17705 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st β(((π(InvβπΆ)π)βπΉ) βfunc πΉ))βπ₯) = ((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ₯))) |
71 | 5, 2, 4 | catcbas 17922 |
. . . . . . . . . . . . . . . 16
β’ (π β π΅ = (π β© Cat)) |
72 | | inss2 4188 |
. . . . . . . . . . . . . . . 16
β’ (π β© Cat) β
Cat |
73 | 71, 72 | eqsstrdi 3997 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β Cat) |
74 | 73, 8 | sseldd 3944 |
. . . . . . . . . . . . . 14
β’ (π β π β Cat) |
75 | 74 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β π β Cat) |
76 | 61, 38, 75, 42 | idfu1 17701 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st
β(idfuncβπ))βπ₯) = π₯) |
77 | 67, 70, 76 | 3eqtr3d 2786 |
. . . . . . . . . . 11
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ₯)) = π₯) |
78 | 66 | fveq1d 6840 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st β(((π(InvβπΆ)π)βπΉ) βfunc πΉ))βπ¦) = ((1st
β(idfuncβπ))βπ¦)) |
79 | 38, 68, 69, 43 | cofu1 17705 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st β(((π(InvβπΆ)π)βπΉ) βfunc πΉ))βπ¦) = ((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ¦))) |
80 | 61, 38, 75, 43 | idfu1 17701 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st
β(idfuncβπ))βπ¦) = π¦) |
81 | 78, 79, 80 | 3eqtr3d 2786 |
. . . . . . . . . . 11
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ¦)) = π¦) |
82 | 77, 81 | oveq12d 7368 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ₯))(Hom βπ)((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ¦))) = (π₯(Hom βπ)π¦)) |
83 | 82 | feq3d 6651 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)):(((1st βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦))βΆ(((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ₯))(Hom βπ)((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ¦))) β (((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)):(((1st βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦))βΆ(π₯(Hom βπ)π¦))) |
84 | 57, 83 | mpbid 231 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)):(((1st βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦))βΆ(π₯(Hom βπ)π¦)) |
85 | 65 | fveq2d 6842 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (2nd β(((π(InvβπΆ)π)βπΉ) βfunc πΉ)) = (2nd
β(idfuncβπ))) |
86 | 85 | oveqd 7367 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (π₯(2nd β(((π(InvβπΆ)π)βπΉ) βfunc πΉ))π¦) = (π₯(2nd
β(idfuncβπ))π¦)) |
87 | 38, 68, 69, 42, 43 | cofu2nd 17706 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (π₯(2nd β(((π(InvβπΆ)π)βπΉ) βfunc πΉ))π¦) = ((((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)) β (π₯(2nd βπΉ)π¦))) |
88 | 61, 38, 75, 39, 42, 43 | idfu2nd 17698 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (π₯(2nd
β(idfuncβπ))π¦) = ( I βΎ (π₯(Hom βπ)π¦))) |
89 | 86, 87, 88 | 3eqtr3d 2786 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)) β (π₯(2nd βπΉ)π¦)) = ( I βΎ (π₯(Hom βπ)π¦))) |
90 | 23 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΉ β (ππΌπ)) β ((π(InvβπΆ)π)βπΉ)(π(SectβπΆ)π)πΉ) |
91 | 2, 25, 26, 27, 21, 14, 16, 15 | issect 17571 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΉ β (ππΌπ)) β (((π(InvβπΆ)π)βπΉ)(π(SectβπΆ)π)πΉ β (((π(InvβπΆ)π)βπΉ) β (π(Hom βπΆ)π) β§ πΉ β (π(Hom βπΆ)π) β§ (πΉ(β¨π, πβ©(compβπΆ)π)((π(InvβπΆ)π)βπΉ)) = ((IdβπΆ)βπ)))) |
92 | 90, 91 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΉ β (ππΌπ)) β (((π(InvβπΆ)π)βπΉ) β (π(Hom βπΆ)π) β§ πΉ β (π(Hom βπΆ)π) β§ (πΉ(β¨π, πβ©(compβπΆ)π)((π(InvβπΆ)π)βπΉ)) = ((IdβπΆ)βπ))) |
93 | 92 | simp3d 1145 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ(β¨π, πβ©(compβπΆ)π)((π(InvβπΆ)π)βπΉ)) = ((IdβπΆ)βπ)) |
94 | 5, 2, 59, 26, 16, 15, 16, 50, 33 | catcco 17926 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ(β¨π, πβ©(compβπΆ)π)((π(InvβπΆ)π)βπΉ)) = (πΉ βfunc ((π(InvβπΆ)π)βπΉ))) |
95 | | eqid 2738 |
. . . . . . . . . . . . . . 15
β’
(idfuncβπ) = (idfuncβπ) |
96 | 5, 2, 27, 95, 4, 9 | catcid 17928 |
. . . . . . . . . . . . . 14
β’ (π β ((IdβπΆ)βπ) = (idfuncβπ)) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ β (ππΌπ)) β ((IdβπΆ)βπ) = (idfuncβπ)) |
98 | 93, 94, 97 | 3eqtr3d 2786 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ βfunc ((π(InvβπΆ)π)βπΉ)) = (idfuncβπ)) |
99 | 98 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (πΉ βfunc ((π(InvβπΆ)π)βπΉ)) = (idfuncβπ)) |
100 | 99 | fveq2d 6842 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (2nd β(πΉ βfunc
((π(InvβπΆ)π)βπΉ))) = (2nd
β(idfuncβπ))) |
101 | 100 | oveqd 7367 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((1st βπΉ)βπ₯)(2nd β(πΉ βfunc ((π(InvβπΆ)π)βπΉ)))((1st βπΉ)βπ¦)) = (((1st βπΉ)βπ₯)(2nd
β(idfuncβπ))((1st βπΉ)βπ¦))) |
102 | 45, 69, 68, 55, 56 | cofu2nd 17706 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((1st βπΉ)βπ₯)(2nd β(πΉ βfunc ((π(InvβπΆ)π)βπΉ)))((1st βπΉ)βπ¦)) = ((((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ₯))(2nd βπΉ)((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ¦))) β (((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)))) |
103 | 77, 81 | oveq12d 7368 |
. . . . . . . . . . 11
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ₯))(2nd βπΉ)((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ¦))) = (π₯(2nd βπΉ)π¦)) |
104 | 103 | coeq1d 5814 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ₯))(2nd βπΉ)((1st β((π(InvβπΆ)π)βπΉ))β((1st βπΉ)βπ¦))) β (((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦))) = ((π₯(2nd βπΉ)π¦) β (((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)))) |
105 | 102, 104 | eqtrd 2778 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((1st βπΉ)βπ₯)(2nd β(πΉ βfunc ((π(InvβπΆ)π)βπΉ)))((1st βπΉ)βπ¦)) = ((π₯(2nd βπΉ)π¦) β (((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦)))) |
106 | 73 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β π΅ β Cat) |
107 | 9 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β π β π΅) |
108 | 106, 107 | sseldd 3944 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β π β Cat) |
109 | 95, 45, 108, 40, 55, 56 | idfu2nd 17698 |
. . . . . . . . 9
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (((1st βπΉ)βπ₯)(2nd
β(idfuncβπ))((1st βπΉ)βπ¦)) = ( I βΎ (((1st
βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦)))) |
110 | 101, 105,
109 | 3eqtr3d 2786 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β ((π₯(2nd βπΉ)π¦) β (((1st βπΉ)βπ₯)(2nd β((π(InvβπΆ)π)βπΉ))((1st βπΉ)βπ¦))) = ( I βΎ (((1st
βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦)))) |
111 | 44, 84, 89, 110 | fcof1od 7235 |
. . . . . . 7
β’ (((π β§ πΉ β (ππΌπ)) β§ (π₯ β π
β§ π¦ β π
)) β (π₯(2nd βπΉ)π¦):(π₯(Hom βπ)π¦)β1-1-ontoβ(((1st βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦))) |
112 | 111 | ralrimivva 3196 |
. . . . . 6
β’ ((π β§ πΉ β (ππΌπ)) β βπ₯ β π
βπ¦ β π
(π₯(2nd βπΉ)π¦):(π₯(Hom βπ)π¦)β1-1-ontoβ(((1st βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦))) |
113 | 38, 39, 40 | isffth2 17738 |
. . . . . 6
β’
((1st βπΉ)((π Full π) β© (π Faith π))(2nd βπΉ) β ((1st βπΉ)(π Func π)(2nd βπΉ) β§ βπ₯ β π
βπ¦ β π
(π₯(2nd βπΉ)π¦):(π₯(Hom βπ)π¦)β1-1-ontoβ(((1st βπΉ)βπ₯)(Hom βπ)((1st βπΉ)βπ¦)))) |
114 | 37, 112, 113 | sylanbrc 584 |
. . . . 5
β’ ((π β§ πΉ β (ππΌπ)) β (1st βπΉ)((π Full π) β© (π Faith π))(2nd βπΉ)) |
115 | | df-br 5105 |
. . . . 5
β’
((1st βπΉ)((π Full π) β© (π Faith π))(2nd βπΉ) β β¨(1st βπΉ), (2nd βπΉ)β© β ((π Full π) β© (π Faith π))) |
116 | 114, 115 | sylib 217 |
. . . 4
β’ ((π β§ πΉ β (ππΌπ)) β β¨(1st βπΉ), (2nd βπΉ)β© β ((π Full π) β© (π Faith π))) |
117 | 35, 116 | eqeltrd 2839 |
. . 3
β’ ((π β§ πΉ β (ππΌπ)) β πΉ β ((π Full π) β© (π Faith π))) |
118 | 38, 45, 37 | funcf1 17687 |
. . . 4
β’ ((π β§ πΉ β (ππΌπ)) β (1st βπΉ):π
βΆπ) |
119 | 45, 38, 52 | funcf1 17687 |
. . . 4
β’ ((π β§ πΉ β (ππΌπ)) β (1st β((π(InvβπΆ)π)βπΉ)):πβΆπ
) |
120 | 64 | fveq2d 6842 |
. . . . 5
β’ ((π β§ πΉ β (ππΌπ)) β (1st β(((π(InvβπΆ)π)βπΉ) βfunc πΉ)) = (1st
β(idfuncβπ))) |
121 | 38, 33, 50 | cofu1st 17704 |
. . . . 5
β’ ((π β§ πΉ β (ππΌπ)) β (1st β(((π(InvβπΆ)π)βπΉ) βfunc πΉ)) = ((1st
β((π(InvβπΆ)π)βπΉ)) β (1st βπΉ))) |
122 | 74 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (ππΌπ)) β π β Cat) |
123 | 61, 38, 122 | idfu1st 17700 |
. . . . 5
β’ ((π β§ πΉ β (ππΌπ)) β (1st
β(idfuncβπ)) = ( I βΎ π
)) |
124 | 120, 121,
123 | 3eqtr3d 2786 |
. . . 4
β’ ((π β§ πΉ β (ππΌπ)) β ((1st β((π(InvβπΆ)π)βπΉ)) β (1st βπΉ)) = ( I βΎ π
)) |
125 | 98 | fveq2d 6842 |
. . . . 5
β’ ((π β§ πΉ β (ππΌπ)) β (1st β(πΉ βfunc
((π(InvβπΆ)π)βπΉ))) = (1st
β(idfuncβπ))) |
126 | 45, 50, 33 | cofu1st 17704 |
. . . . 5
β’ ((π β§ πΉ β (ππΌπ)) β (1st β(πΉ βfunc
((π(InvβπΆ)π)βπΉ))) = ((1st βπΉ) β (1st
β((π(InvβπΆ)π)βπΉ)))) |
127 | 73, 9 | sseldd 3944 |
. . . . . . 7
β’ (π β π β Cat) |
128 | 127 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (ππΌπ)) β π β Cat) |
129 | 95, 45, 128 | idfu1st 17700 |
. . . . 5
β’ ((π β§ πΉ β (ππΌπ)) β (1st
β(idfuncβπ)) = ( I βΎ π)) |
130 | 125, 126,
129 | 3eqtr3d 2786 |
. . . 4
β’ ((π β§ πΉ β (ππΌπ)) β ((1st βπΉ) β (1st
β((π(InvβπΆ)π)βπΉ))) = ( I βΎ π)) |
131 | 118, 119,
124, 130 | fcof1od 7235 |
. . 3
β’ ((π β§ πΉ β (ππΌπ)) β (1st βπΉ):π
β1-1-ontoβπ) |
132 | 117, 131 | jca 513 |
. 2
β’ ((π β§ πΉ β (ππΌπ)) β (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) |
133 | 7 | adantr 482 |
. . 3
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β πΆ β Cat) |
134 | 8 | adantr 482 |
. . 3
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β π β π΅) |
135 | 9 | adantr 482 |
. . 3
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β π β π΅) |
136 | | inss1 4187 |
. . . . . . 7
β’ ((π Full π) β© (π Faith π)) β (π Full π) |
137 | | fullfunc 17728 |
. . . . . . 7
β’ (π Full π) β (π Func π) |
138 | 136, 137 | sstri 3952 |
. . . . . 6
β’ ((π Full π) β© (π Faith π)) β (π Func π) |
139 | | simprl 770 |
. . . . . 6
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β πΉ β ((π Full π) β© (π Faith π))) |
140 | 138, 139 | sselid 3941 |
. . . . 5
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β πΉ β (π Func π)) |
141 | 1, 140, 34 | sylancr 588 |
. . . 4
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β πΉ = β¨(1st βπΉ), (2nd βπΉ)β©) |
142 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β π β π) |
143 | | eqid 2738 |
. . . . 5
β’ (π₯ β π, π¦ β π β¦ β‘((β‘(1st βπΉ)βπ₯)(2nd βπΉ)(β‘(1st βπΉ)βπ¦))) = (π₯ β π, π¦ β π β¦ β‘((β‘(1st βπΉ)βπ₯)(2nd βπΉ)(β‘(1st βπΉ)βπ¦))) |
144 | 141, 139 | eqeltrrd 2840 |
. . . . . 6
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β β¨(1st
βπΉ), (2nd
βπΉ)β© β
((π Full π) β© (π Faith π))) |
145 | 144, 115 | sylibr 233 |
. . . . 5
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β (1st
βπΉ)((π Full π) β© (π Faith π))(2nd βπΉ)) |
146 | | simprr 772 |
. . . . 5
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β (1st
βπΉ):π
β1-1-ontoβπ) |
147 | 5, 2, 38, 45, 142, 134, 135, 3, 143, 145, 146 | catcisolem 17931 |
. . . 4
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β β¨(1st
βπΉ), (2nd
βπΉ)β©(π(InvβπΆ)π)β¨β‘(1st βπΉ), (π₯ β π, π¦ β π β¦ β‘((β‘(1st βπΉ)βπ₯)(2nd βπΉ)(β‘(1st βπΉ)βπ¦)))β©) |
148 | 141, 147 | eqbrtrd 5126 |
. . 3
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β πΉ(π(InvβπΆ)π)β¨β‘(1st βπΉ), (π₯ β π, π¦ β π β¦ β‘((β‘(1st βπΉ)βπ₯)(2nd βπΉ)(β‘(1st βπΉ)βπ¦)))β©) |
149 | 2, 3, 133, 134, 135, 10, 148 | inviso1 17584 |
. 2
β’ ((π β§ (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ)) β πΉ β (ππΌπ)) |
150 | 132, 149 | impbida 800 |
1
β’ (π β (πΉ β (ππΌπ) β (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π
β1-1-ontoβπ))) |