Step | Hyp | Ref
| Expression |
1 | | fuciso.q |
. . . . . 6
β’ π = (πΆ FuncCat π·) |
2 | 1 | fucbas 17783 |
. . . . 5
β’ (πΆ Func π·) = (Baseβπ) |
3 | | fuciso.n |
. . . . . 6
β’ π = (πΆ Nat π·) |
4 | 1, 3 | fuchom 17784 |
. . . . 5
β’ π = (Hom βπ) |
5 | | fuciso.i |
. . . . 5
β’ πΌ = (Isoβπ) |
6 | | fuciso.f |
. . . . . . . 8
β’ (π β πΉ β (πΆ Func π·)) |
7 | | funcrcl 17684 |
. . . . . . . 8
β’ (πΉ β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
8 | 6, 7 | syl 17 |
. . . . . . 7
β’ (π β (πΆ β Cat β§ π· β Cat)) |
9 | 8 | simpld 496 |
. . . . . 6
β’ (π β πΆ β Cat) |
10 | 8 | simprd 497 |
. . . . . 6
β’ (π β π· β Cat) |
11 | 1, 9, 10 | fuccat 17794 |
. . . . 5
β’ (π β π β Cat) |
12 | | fuciso.g |
. . . . 5
β’ (π β πΊ β (πΆ Func π·)) |
13 | 2, 4, 5, 11, 6, 12 | isohom 17594 |
. . . 4
β’ (π β (πΉπΌπΊ) β (πΉππΊ)) |
14 | 13 | sselda 3943 |
. . 3
β’ ((π β§ π΄ β (πΉπΌπΊ)) β π΄ β (πΉππΊ)) |
15 | | eqid 2738 |
. . . . 5
β’
(Baseβπ·) =
(Baseβπ·) |
16 | | eqid 2738 |
. . . . 5
β’
(Invβπ·) =
(Invβπ·) |
17 | 10 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π΄ β (πΉπΌπΊ)) β§ π₯ β π΅) β π· β Cat) |
18 | | fuciso.b |
. . . . . . . 8
β’ π΅ = (BaseβπΆ) |
19 | | relfunc 17683 |
. . . . . . . . 9
β’ Rel
(πΆ Func π·) |
20 | | 1st2ndbr 7964 |
. . . . . . . . 9
β’ ((Rel
(πΆ Func π·) β§ πΉ β (πΆ Func π·)) β (1st βπΉ)(πΆ Func π·)(2nd βπΉ)) |
21 | 19, 6, 20 | sylancr 588 |
. . . . . . . 8
β’ (π β (1st
βπΉ)(πΆ Func π·)(2nd βπΉ)) |
22 | 18, 15, 21 | funcf1 17687 |
. . . . . . 7
β’ (π β (1st
βπΉ):π΅βΆ(Baseβπ·)) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β (πΉπΌπΊ)) β (1st βπΉ):π΅βΆ(Baseβπ·)) |
24 | 23 | ffvelcdmda 7030 |
. . . . 5
β’ (((π β§ π΄ β (πΉπΌπΊ)) β§ π₯ β π΅) β ((1st βπΉ)βπ₯) β (Baseβπ·)) |
25 | | 1st2ndbr 7964 |
. . . . . . . . 9
β’ ((Rel
(πΆ Func π·) β§ πΊ β (πΆ Func π·)) β (1st βπΊ)(πΆ Func π·)(2nd βπΊ)) |
26 | 19, 12, 25 | sylancr 588 |
. . . . . . . 8
β’ (π β (1st
βπΊ)(πΆ Func π·)(2nd βπΊ)) |
27 | 18, 15, 26 | funcf1 17687 |
. . . . . . 7
β’ (π β (1st
βπΊ):π΅βΆ(Baseβπ·)) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β (πΉπΌπΊ)) β (1st βπΊ):π΅βΆ(Baseβπ·)) |
29 | 28 | ffvelcdmda 7030 |
. . . . 5
β’ (((π β§ π΄ β (πΉπΌπΊ)) β§ π₯ β π΅) β ((1st βπΊ)βπ₯) β (Baseβπ·)) |
30 | | fuciso.j |
. . . . 5
β’ π½ = (Isoβπ·) |
31 | | eqid 2738 |
. . . . . . . . . . . 12
β’
(Invβπ) =
(Invβπ) |
32 | 2, 31, 11, 6, 12, 5 | isoval 17583 |
. . . . . . . . . . 11
β’ (π β (πΉπΌπΊ) = dom (πΉ(Invβπ)πΊ)) |
33 | 32 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π β (π΄ β (πΉπΌπΊ) β π΄ β dom (πΉ(Invβπ)πΊ))) |
34 | 2, 31, 11, 6, 12 | invfun 17582 |
. . . . . . . . . . 11
β’ (π β Fun (πΉ(Invβπ)πΊ)) |
35 | | funfvbrb 6997 |
. . . . . . . . . . 11
β’ (Fun
(πΉ(Invβπ)πΊ) β (π΄ β dom (πΉ(Invβπ)πΊ) β π΄(πΉ(Invβπ)πΊ)((πΉ(Invβπ)πΊ)βπ΄))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
β’ (π β (π΄ β dom (πΉ(Invβπ)πΊ) β π΄(πΉ(Invβπ)πΊ)((πΉ(Invβπ)πΊ)βπ΄))) |
37 | 33, 36 | bitrd 279 |
. . . . . . . . 9
β’ (π β (π΄ β (πΉπΌπΊ) β π΄(πΉ(Invβπ)πΊ)((πΉ(Invβπ)πΊ)βπ΄))) |
38 | 37 | biimpa 478 |
. . . . . . . 8
β’ ((π β§ π΄ β (πΉπΌπΊ)) β π΄(πΉ(Invβπ)πΊ)((πΉ(Invβπ)πΊ)βπ΄)) |
39 | 1, 18, 3, 6, 12, 31, 16 | fucinv 17797 |
. . . . . . . . 9
β’ (π β (π΄(πΉ(Invβπ)πΊ)((πΉ(Invβπ)πΊ)βπ΄) β (π΄ β (πΉππΊ) β§ ((πΉ(Invβπ)πΊ)βπ΄) β (πΊππΉ) β§ βπ₯ β π΅ (π΄βπ₯)(((1st βπΉ)βπ₯)(Invβπ·)((1st βπΊ)βπ₯))(((πΉ(Invβπ)πΊ)βπ΄)βπ₯)))) |
40 | 39 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΄ β (πΉπΌπΊ)) β (π΄(πΉ(Invβπ)πΊ)((πΉ(Invβπ)πΊ)βπ΄) β (π΄ β (πΉππΊ) β§ ((πΉ(Invβπ)πΊ)βπ΄) β (πΊππΉ) β§ βπ₯ β π΅ (π΄βπ₯)(((1st βπΉ)βπ₯)(Invβπ·)((1st βπΊ)βπ₯))(((πΉ(Invβπ)πΊ)βπ΄)βπ₯)))) |
41 | 38, 40 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π΄ β (πΉπΌπΊ)) β (π΄ β (πΉππΊ) β§ ((πΉ(Invβπ)πΊ)βπ΄) β (πΊππΉ) β§ βπ₯ β π΅ (π΄βπ₯)(((1st βπΉ)βπ₯)(Invβπ·)((1st βπΊ)βπ₯))(((πΉ(Invβπ)πΊ)βπ΄)βπ₯))) |
42 | 41 | simp3d 1145 |
. . . . . 6
β’ ((π β§ π΄ β (πΉπΌπΊ)) β βπ₯ β π΅ (π΄βπ₯)(((1st βπΉ)βπ₯)(Invβπ·)((1st βπΊ)βπ₯))(((πΉ(Invβπ)πΊ)βπ΄)βπ₯)) |
43 | 42 | r19.21bi 3233 |
. . . . 5
β’ (((π β§ π΄ β (πΉπΌπΊ)) β§ π₯ β π΅) β (π΄βπ₯)(((1st βπΉ)βπ₯)(Invβπ·)((1st βπΊ)βπ₯))(((πΉ(Invβπ)πΊ)βπ΄)βπ₯)) |
44 | 15, 16, 17, 24, 29, 30, 43 | inviso1 17584 |
. . . 4
β’ (((π β§ π΄ β (πΉπΌπΊ)) β§ π₯ β π΅) β (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))) |
45 | 44 | ralrimiva 3142 |
. . 3
β’ ((π β§ π΄ β (πΉπΌπΊ)) β βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))) |
46 | 14, 45 | jca 513 |
. 2
β’ ((π β§ π΄ β (πΉπΌπΊ)) β (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) |
47 | 11 | adantr 482 |
. . 3
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β π β Cat) |
48 | 6 | adantr 482 |
. . 3
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β πΉ β (πΆ Func π·)) |
49 | 12 | adantr 482 |
. . 3
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β πΊ β (πΆ Func π·)) |
50 | | simprl 770 |
. . . 4
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β π΄ β (πΉππΊ)) |
51 | 10 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β§ π¦ β π΅) β π· β Cat) |
52 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β (1st βπΉ):π΅βΆ(Baseβπ·)) |
53 | 52 | ffvelcdmda 7030 |
. . . . 5
β’ (((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β§ π¦ β π΅) β ((1st βπΉ)βπ¦) β (Baseβπ·)) |
54 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β (1st βπΊ):π΅βΆ(Baseβπ·)) |
55 | 54 | ffvelcdmda 7030 |
. . . . 5
β’ (((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β§ π¦ β π΅) β ((1st βπΊ)βπ¦) β (Baseβπ·)) |
56 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))) |
57 | | fveq2 6838 |
. . . . . . . 8
β’ (π₯ = π¦ β (π΄βπ₯) = (π΄βπ¦)) |
58 | | fveq2 6838 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((1st βπΉ)βπ₯) = ((1st βπΉ)βπ¦)) |
59 | | fveq2 6838 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((1st βπΊ)βπ₯) = ((1st βπΊ)βπ¦)) |
60 | 58, 59 | oveq12d 7368 |
. . . . . . . 8
β’ (π₯ = π¦ β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)) = (((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))) |
61 | 57, 60 | eleq12d 2833 |
. . . . . . 7
β’ (π₯ = π¦ β ((π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)) β (π΄βπ¦) β (((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦)))) |
62 | 61 | rspccva 3579 |
. . . . . 6
β’
((βπ₯ β
π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)) β§ π¦ β π΅) β (π΄βπ¦) β (((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))) |
63 | 56, 62 | sylan 581 |
. . . . 5
β’ (((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β§ π¦ β π΅) β (π΄βπ¦) β (((1st βπΉ)βπ¦)π½((1st βπΊ)βπ¦))) |
64 | 15, 30, 16, 51, 53, 55, 63 | invisoinvr 17609 |
. . . 4
β’ (((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β§ π¦ β π΅) β (π΄βπ¦)(((1st βπΉ)βπ¦)(Invβπ·)((1st βπΊ)βπ¦))((((1st βπΉ)βπ¦)(Invβπ·)((1st βπΊ)βπ¦))β(π΄βπ¦))) |
65 | 1, 18, 3, 48, 49, 31, 16, 50, 64 | invfuc 17798 |
. . 3
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β π΄(πΉ(Invβπ)πΊ)(π¦ β π΅ β¦ ((((1st βπΉ)βπ¦)(Invβπ·)((1st βπΊ)βπ¦))β(π΄βπ¦)))) |
66 | 2, 31, 47, 48, 49, 5, 65 | inviso1 17584 |
. 2
β’ ((π β§ (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)))) β π΄ β (πΉπΌπΊ)) |
67 | 46, 66 | impbida 800 |
1
β’ (π β (π΄ β (πΉπΌπΊ) β (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))))) |