Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(BaseβπΆ) =
(BaseβπΆ) |
2 | | eqid 2733 |
. . 3
β’ (Hom
βπΆ) = (Hom
βπΆ) |
3 | | eqid 2733 |
. . 3
β’
(compβπΆ) =
(compβπΆ) |
4 | | eqid 2733 |
. . 3
β’
(IdβπΆ) =
(IdβπΆ) |
5 | | setcsect.n |
. . 3
β’ π = (SectβπΆ) |
6 | | setcmon.u |
. . . 4
β’ (π β π β π) |
7 | | setcmon.c |
. . . . 5
β’ πΆ = (SetCatβπ) |
8 | 7 | setccat 17976 |
. . . 4
β’ (π β π β πΆ β Cat) |
9 | 6, 8 | syl 17 |
. . 3
β’ (π β πΆ β Cat) |
10 | | setcmon.x |
. . . 4
β’ (π β π β π) |
11 | 7, 6 | setcbas 17969 |
. . . 4
β’ (π β π = (BaseβπΆ)) |
12 | 10, 11 | eleqtrd 2836 |
. . 3
β’ (π β π β (BaseβπΆ)) |
13 | | setcmon.y |
. . . 4
β’ (π β π β π) |
14 | 13, 11 | eleqtrd 2836 |
. . 3
β’ (π β π β (BaseβπΆ)) |
15 | 1, 2, 3, 4, 5, 9, 12, 14 | issect 17641 |
. 2
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)))) |
16 | 7, 6, 2, 10, 13 | elsetchom 17972 |
. . . . . 6
β’ (π β (πΉ β (π(Hom βπΆ)π) β πΉ:πβΆπ)) |
17 | 7, 6, 2, 13, 10 | elsetchom 17972 |
. . . . . 6
β’ (π β (πΊ β (π(Hom βπΆ)π) β πΊ:πβΆπ)) |
18 | 16, 17 | anbi12d 632 |
. . . . 5
β’ (π β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β (πΉ:πβΆπ β§ πΊ:πβΆπ))) |
19 | 18 | anbi1d 631 |
. . . 4
β’ (π β (((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ:πβΆπ β§ πΊ:πβΆπ) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)))) |
20 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β π β π) |
21 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β π β π) |
22 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β π β π) |
23 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β πΉ:πβΆπ) |
24 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β πΊ:πβΆπ) |
25 | 7, 20, 3, 21, 22, 21, 23, 24 | setcco 17974 |
. . . . . 6
β’ ((π β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = (πΊ β πΉ)) |
26 | 7, 4, 6, 10 | setcid 17977 |
. . . . . . 7
β’ (π β ((IdβπΆ)βπ) = ( I βΎ π)) |
27 | 26 | adantr 482 |
. . . . . 6
β’ ((π β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β ((IdβπΆ)βπ) = ( I βΎ π)) |
28 | 25, 27 | eqeq12d 2749 |
. . . . 5
β’ ((π β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β ((πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ) β (πΊ β πΉ) = ( I βΎ π))) |
29 | 28 | pm5.32da 580 |
. . . 4
β’ (π β (((πΉ:πβΆπ β§ πΊ:πβΆπ) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ:πβΆπ β§ πΊ:πβΆπ) β§ (πΊ β πΉ) = ( I βΎ π)))) |
30 | 19, 29 | bitrd 279 |
. . 3
β’ (π β (((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ:πβΆπ β§ πΊ:πβΆπ) β§ (πΊ β πΉ) = ( I βΎ π)))) |
31 | | df-3an 1090 |
. . 3
β’ ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π)) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ))) |
32 | | df-3an 1090 |
. . 3
β’ ((πΉ:πβΆπ β§ πΊ:πβΆπ β§ (πΊ β πΉ) = ( I βΎ π)) β ((πΉ:πβΆπ β§ πΊ:πβΆπ) β§ (πΊ β πΉ) = ( I βΎ π))) |
33 | 30, 31, 32 | 3bitr4g 314 |
. 2
β’ (π β ((πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) β (πΉ:πβΆπ β§ πΊ:πβΆπ β§ (πΊ β πΉ) = ( I βΎ π)))) |
34 | 15, 33 | bitrd 279 |
1
β’ (π β (πΉ(πππ)πΊ β (πΉ:πβΆπ β§ πΊ:πβΆπ β§ (πΊ β πΉ) = ( I βΎ π)))) |