This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to C = MndToCat (M)$
		mndtccat.m	$⊢ φ \to M \in Mnd$
		mndtcid.b	$⊢ φ \to B = {Base}_{C}$
		mndtcid.x	$⊢ φ \to X \in B$
		mndtcid.i	$⊢ φ \to \underset{˙}{1} = Id (C)$
	Assertion	mndtcid	$⊢ φ \to \underset{˙}{1} (X) = 0_{M}$

Proof

Step	Hyp	Ref	Expression
1		mndtccat.c	$⊢ φ \to C = MndToCat (M)$
2		mndtccat.m	$⊢ φ \to M \in Mnd$
3		mndtcid.b	$⊢ φ \to B = {Base}_{C}$
4		mndtcid.x	$⊢ φ \to X \in B$
5		mndtcid.i	$⊢ φ \to \underset{˙}{1} = Id (C)$
6	1 2	mndtccatid	$⊢ φ \to (C \in Cat \land Id (C) = (x \in {Base}_{C} ⟼ 0_{M}))$
7	6	simprd	$⊢ φ \to Id (C) = (x \in {Base}_{C} ⟼ 0_{M})$
8	5 7	eqtrd	$⊢ φ \to \underset{˙}{1} = (x \in {Base}_{C} ⟼ 0_{M})$
9		eqidd	$⊢ (φ \land x = X) \to 0_{M} = 0_{M}$
10	4 3	eleqtrd	$⊢ φ \to X \in {Base}_{C}$
11		fvexd	$⊢ φ \to 0_{M} \in V$
12	8 9 10 11	fvmptd	$⊢ φ \to \underset{˙}{1} (X) = 0_{M}$