Theorem mndtcbas

Description: The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024)

	Ref	Expression
Hypotheses	mndtcbas.c	No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
	mndtcbas.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	mndtcbas.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
Assertion	mndtcbas	$$⊢\phi \to \exists !xx\in B$$

Proof

Step	Hyp	Ref	Expression
1		mndtcbas.c	Could not format ( ph -> C = ( MndToCat ` M ) ) : No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
2		mndtcbas.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		mndtcbas.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
4	1 2 3	mndtcbasval	$$⊢\phi \to B=\left\{M\right\}$$
5		sneq	$$⊢x=M\to \left\{x\right\}=\left\{M\right\}$$
6	5	eqeq2d	$$⊢x=M\to \left(B=\left\{x\right\}\leftrightarrow B=\left\{M\right\}\right)$$
7	2 4 6	spcedv	$$⊢\phi \to \exists xB=\left\{x\right\}$$
8		eusn	$$⊢\exists !xx\in B\leftrightarrow \exists xB=\left\{x\right\}$$
9	7 8	sylibr	$$⊢\phi \to \exists !xx\in B$$