Step | Hyp | Ref
| Expression |
1 | | idmon.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | idmon.h |
. . 3
β’ π» = (Hom βπΆ) |
3 | | idmon.i |
. . 3
β’ 1 =
(IdβπΆ) |
4 | | idmon.c |
. . 3
β’ (π β πΆ β Cat) |
5 | | idmon.x |
. . 3
β’ (π β π β π΅) |
6 | 1, 2, 3, 4, 5 | catidcl 17632 |
. 2
β’ (π β ( 1 βπ) β (ππ»π)) |
7 | 4 | adantr 479 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β πΆ β Cat) |
8 | | simpr1 1192 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β π§ β π΅) |
9 | | eqid 2730 |
. . . . . 6
β’
(compβπΆ) =
(compβπΆ) |
10 | 5 | adantr 479 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β π β π΅) |
11 | | simpr2 1193 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β π β (π§π»π)) |
12 | 1, 2, 3, 7, 8, 9, 10, 11 | catlid 17633 |
. . . . 5
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β (( 1 βπ)(β¨π§, πβ©(compβπΆ)π)π) = π) |
13 | | simpr3 1194 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β β β (π§π»π)) |
14 | 1, 2, 3, 7, 8, 9, 10, 13 | catlid 17633 |
. . . . 5
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β (( 1 βπ)(β¨π§, πβ©(compβπΆ)π)β) = β) |
15 | 12, 14 | eqeq12d 2746 |
. . . 4
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β ((( 1 βπ)(β¨π§, πβ©(compβπΆ)π)π) = (( 1 βπ)(β¨π§, πβ©(compβπΆ)π)β) β π = β)) |
16 | 15 | biimpd 228 |
. . 3
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β ((( 1 βπ)(β¨π§, πβ©(compβπΆ)π)π) = (( 1 βπ)(β¨π§, πβ©(compβπΆ)π)β) β π = β)) |
17 | 16 | ralrimivvva 3201 |
. 2
β’ (π β βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((( 1 βπ)(β¨π§, πβ©(compβπΆ)π)π) = (( 1 βπ)(β¨π§, πβ©(compβπΆ)π)β) β π = β)) |
18 | | idmon.m |
. . 3
β’ π = (MonoβπΆ) |
19 | 1, 2, 9, 18, 4, 5,
5 | ismon2 17687 |
. 2
β’ (π β (( 1 βπ) β (πππ) β (( 1 βπ) β (ππ»π) β§ βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((( 1 βπ)(β¨π§, πβ©(compβπΆ)π)π) = (( 1 βπ)(β¨π§, πβ©(compβπΆ)π)β) β π = β)))) |
20 | 6, 17, 19 | mpbir2and 709 |
1
β’ (π β ( 1 βπ) β (πππ)) |