Theorem mndtcid

Description: The identity morphism, or identity arrow, of the category built from a monoid is the identity element of the monoid. (Contributed by Zhi Wang, 22-Sep-2024)

	Ref	Expression
Hypotheses	mndtccat.c	No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
	mndtccat.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	mndtcid.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
	mndtcid.x	$$⊢\phi \to X\in B$$
	mndtcid.i	$$⊢\phi \to \underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
Assertion	mndtcid	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=0_M$$

Proof

Step	Hyp	Ref	Expression
1		mndtccat.c	Could not format ( ph -> C = ( MndToCat ` M ) ) : No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
2		mndtccat.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		mndtcid.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
4		mndtcid.x	$$⊢\phi \to X\in B$$
5		mndtcid.i	$$⊢\phi \to \underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
6	1 2	mndtccatid	$$⊢\phi \to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in {\mathrm{Base}}_C⟼0_M\right)\right)$$
7	6	simprd	$$⊢\phi \to \mathrm{Id}\left(C\right)=\left(x\in {\mathrm{Base}}_C⟼0_M\right)$$
8	5 7	eqtrd	$$⊢\phi \to \underset{\dot{}}{1}=\left(x\in {\mathrm{Base}}_C⟼0_M\right)$$
9		eqidd	$$⊢\left(\phi \wedge x=X\right)\to 0_M=0_M$$
10	4 3	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
11		fvexd	$$⊢\phi \to 0_M\in \mathrm{V}$$
12	8 9 10 11	fvmptd	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=0_M$$