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	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
	mndtcbas.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
	mndtcbas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
Assertion	mndtcbas	⊢ ( 𝜑 → ∃! 𝑥 𝑥 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mndtcbas.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2		mndtcbas.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3		mndtcbas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4	1 2 3	mndtcbasval	⊢ ( 𝜑 → 𝐵 = { 𝑀 } )
5		sneq	⊢ ( 𝑥 = 𝑀 → { 𝑥 } = { 𝑀 } )
6	5	eqeq2d	⊢ ( 𝑥 = 𝑀 → ( 𝐵 = { 𝑥 } ↔ 𝐵 = { 𝑀 } ) )
7	2 4 6	spcedv	⊢ ( 𝜑 → ∃ 𝑥 𝐵 = { 𝑥 } )
8		eusn	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐵 ↔ ∃ 𝑥 𝐵 = { 𝑥 } )
9	7 8	sylibr	⊢ ( 𝜑 → ∃! 𝑥 𝑥 ∈ 𝐵 )