Step | Hyp | Ref
| Expression |
1 | | simpr1 1194 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β π§ β π΅) |
2 | | thincid.x |
. . . . . . 7
β’ (π β π β π΅) |
3 | 2 | adantr 481 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β π β π΅) |
4 | | simpr2 1195 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β π β (π§π»π)) |
5 | | simpr3 1196 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β β β (π§π»π)) |
6 | | thincid.b |
. . . . . 6
β’ π΅ = (BaseβπΆ) |
7 | | thincid.h |
. . . . . 6
β’ π» = (Hom βπΆ) |
8 | | thincid.c |
. . . . . . 7
β’ (π β πΆ β ThinCat) |
9 | 8 | adantr 481 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β πΆ β ThinCat) |
10 | 1, 3, 4, 5, 6, 7, 9 | thincmo2 47201 |
. . . . 5
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β π = β) |
11 | 10 | a1d 25 |
. . . 4
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ β β (π§π»π))) β ((π(β¨π§, πβ©(compβπΆ)π)π) = (π(β¨π§, πβ©(compβπΆ)π)β) β π = β)) |
12 | 11 | ralrimivvva 3202 |
. . 3
β’ (π β βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((π(β¨π§, πβ©(compβπΆ)π)π) = (π(β¨π§, πβ©(compβπΆ)π)β) β π = β)) |
13 | | eqid 2731 |
. . . 4
β’
(compβπΆ) =
(compβπΆ) |
14 | | thincmon.m |
. . . 4
β’ π = (MonoβπΆ) |
15 | 8 | thinccd 47198 |
. . . 4
β’ (π β πΆ β Cat) |
16 | | thincmon.y |
. . . 4
β’ (π β π β π΅) |
17 | 6, 7, 13, 14, 15, 2, 16 | ismon2 17646 |
. . 3
β’ (π β (π β (πππ) β (π β (ππ»π) β§ βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((π(β¨π§, πβ©(compβπΆ)π)π) = (π(β¨π§, πβ©(compβπΆ)π)β) β π = β)))) |
18 | 12, 17 | mpbiran2d 706 |
. 2
β’ (π β (π β (πππ) β π β (ππ»π))) |
19 | 18 | eqrdv 2729 |
1
β’ (π β (πππ) = (ππ»π)) |