Step | Hyp | Ref
| Expression |
1 | | fuciso.q |
. . . 4
β’ π = (πΆ FuncCat π·) |
2 | | fuciso.b |
. . . 4
β’ π΅ = (BaseβπΆ) |
3 | | fuciso.n |
. . . 4
β’ π = (πΆ Nat π·) |
4 | | fuciso.f |
. . . 4
β’ (π β πΉ β (πΆ Func π·)) |
5 | | fuciso.g |
. . . 4
β’ (π β πΊ β (πΆ Func π·)) |
6 | | eqid 2733 |
. . . 4
β’
(Sectβπ) =
(Sectβπ) |
7 | | eqid 2733 |
. . . 4
β’
(Sectβπ·) =
(Sectβπ·) |
8 | 1, 2, 3, 4, 5, 6, 7 | fucsect 17866 |
. . 3
β’ (π β (π(πΉ(Sectβπ)πΊ)π β (π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯)))) |
9 | 1, 2, 3, 5, 4, 6, 7 | fucsect 17866 |
. . 3
β’ (π β (π(πΊ(Sectβπ)πΉ)π β (π β (πΊππΉ) β§ π β (πΉππΊ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)))) |
10 | 8, 9 | anbi12d 632 |
. 2
β’ (π β ((π(πΉ(Sectβπ)πΊ)π β§ π(πΊ(Sectβπ)πΉ)π) β ((π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯)) β§ (π β (πΊππΉ) β§ π β (πΉππΊ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))))) |
11 | 1 | fucbas 17853 |
. . 3
β’ (πΆ Func π·) = (Baseβπ) |
12 | | fucinv.i |
. . 3
β’ πΌ = (Invβπ) |
13 | | funcrcl 17754 |
. . . . . 6
β’ (πΉ β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
14 | 4, 13 | syl 17 |
. . . . 5
β’ (π β (πΆ β Cat β§ π· β Cat)) |
15 | 14 | simpld 496 |
. . . 4
β’ (π β πΆ β Cat) |
16 | 14 | simprd 497 |
. . . 4
β’ (π β π· β Cat) |
17 | 1, 15, 16 | fuccat 17864 |
. . 3
β’ (π β π β Cat) |
18 | 11, 12, 17, 4, 5, 6 | isinv 17648 |
. 2
β’ (π β (π(πΉπΌπΊ)π β (π(πΉ(Sectβπ)πΊ)π β§ π(πΊ(Sectβπ)πΉ)π))) |
19 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ·) =
(Baseβπ·) |
20 | | fucinv.j |
. . . . . . 7
β’ π½ = (Invβπ·) |
21 | 16 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β π· β Cat) |
22 | | relfunc 17753 |
. . . . . . . . . 10
β’ Rel
(πΆ Func π·) |
23 | | 1st2ndbr 7975 |
. . . . . . . . . 10
β’ ((Rel
(πΆ Func π·) β§ πΉ β (πΆ Func π·)) β (1st βπΉ)(πΆ Func π·)(2nd βπΉ)) |
24 | 22, 4, 23 | sylancr 588 |
. . . . . . . . 9
β’ (π β (1st
βπΉ)(πΆ Func π·)(2nd βπΉ)) |
25 | 2, 19, 24 | funcf1 17757 |
. . . . . . . 8
β’ (π β (1st
βπΉ):π΅βΆ(Baseβπ·)) |
26 | 25 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((1st βπΉ)βπ₯) β (Baseβπ·)) |
27 | | 1st2ndbr 7975 |
. . . . . . . . . 10
β’ ((Rel
(πΆ Func π·) β§ πΊ β (πΆ Func π·)) β (1st βπΊ)(πΆ Func π·)(2nd βπΊ)) |
28 | 22, 5, 27 | sylancr 588 |
. . . . . . . . 9
β’ (π β (1st
βπΊ)(πΆ Func π·)(2nd βπΊ)) |
29 | 2, 19, 28 | funcf1 17757 |
. . . . . . . 8
β’ (π β (1st
βπΊ):π΅βΆ(Baseβπ·)) |
30 | 29 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((1st βπΊ)βπ₯) β (Baseβπ·)) |
31 | 19, 20, 21, 26, 30, 7 | isinv 17648 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β ((πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯) β ((πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯) β§ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)))) |
32 | 31 | ralbidva 3169 |
. . . . 5
β’ (π β (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯) β βπ₯ β π΅ ((πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯) β§ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)))) |
33 | | r19.26 3111 |
. . . . 5
β’
(βπ₯ β
π΅ ((πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯) β§ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)) β (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))) |
34 | 32, 33 | bitrdi 287 |
. . . 4
β’ (π β (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯) β (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)))) |
35 | 34 | anbi2d 630 |
. . 3
β’ (π β (((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯)) β ((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))))) |
36 | | df-3an 1090 |
. . 3
β’ ((π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯)) β ((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯))) |
37 | | df-3an 1090 |
. . . . 5
β’ ((π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯)) β ((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯))) |
38 | | 3ancoma 1099 |
. . . . . 6
β’ ((π β (πΊππΉ) β§ π β (πΉππΊ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)) β (π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))) |
39 | | df-3an 1090 |
. . . . . 6
β’ ((π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)) β ((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))) |
40 | 38, 39 | bitri 275 |
. . . . 5
β’ ((π β (πΊππΉ) β§ π β (πΉππΊ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)) β ((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))) |
41 | 37, 40 | anbi12i 628 |
. . . 4
β’ (((π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯)) β§ (π β (πΊππΉ) β§ π β (πΉππΊ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))) β (((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯)) β§ ((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)))) |
42 | | anandi 675 |
. . . 4
β’ (((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))) β (((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯)) β§ ((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)))) |
43 | 41, 42 | bitr4i 278 |
. . 3
β’ (((π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯)) β§ (π β (πΊππΉ) β§ π β (πΉππΊ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))) β ((π β (πΉππΊ) β§ π β (πΊππΉ)) β§ (βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯)))) |
44 | 35, 36, 43 | 3bitr4g 314 |
. 2
β’ (π β ((π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯)) β ((π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)(Sectβπ·)((1st βπΊ)βπ₯))(πβπ₯)) β§ (π β (πΊππΉ) β§ π β (πΉππΊ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΊ)βπ₯)(Sectβπ·)((1st βπΉ)βπ₯))(πβπ₯))))) |
45 | 10, 18, 44 | 3bitr4d 311 |
1
β’ (π β (π(πΉπΌπΊ)π β (π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯)))) |