Metamath Proof Explorer
Description: The category built from a monoid contains precisely one object.
(Contributed by Zhi Wang, 22-Sep-2024)
|
|
Ref |
Expression |
|
Hypotheses |
mndtcbas.c |
|
|
|
mndtcbas.m |
|
|
|
mndtcbas.b |
|
|
Assertion |
mndtcbas |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
mndtcbas.c |
|
2 |
|
mndtcbas.m |
|
3 |
|
mndtcbas.b |
|
4 |
1 2 3
|
mndtcbasval |
|
5 |
|
sneq |
|
6 |
5
|
eqeq2d |
|
7 |
2 4 6
|
spcedv |
|
8 |
|
eusn |
|
9 |
7 8
|
sylibr |
|