Theorem mndtcbaseu

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

	Ref	Expression
Hypotheses	mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
	mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
	mndtcbaseu.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
Assertion	mndtcbaseu	⊢ ( 𝜑 → ∃! 𝑥 𝑥 ∈ 𝐵 )

Proof

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