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 ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
mndtcid.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
mndtcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mndtcid.i ⊢ ( 𝜑 → 1 = ( Id ‘ 𝐶 ) )
Assertion mndtcid ( 𝜑 → ( 1 ‘ 𝑋 ) = ( 0g ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 mndtccat.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2 mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 mndtcid.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4 mndtcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 mndtcid.i ⊢ ( 𝜑 → 1 = ( Id ‘ 𝐶 ) )
6 1 2 mndtccatid ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 0g ‘ 𝑀 ) ) ) )
7 6 simprd ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 0g ‘ 𝑀 ) ) )
8 5 7 eqtrd ⊢ ( 𝜑 → 1 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 0g ‘ 𝑀 ) ) )
9 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 ) )
10 4 3 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
11 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑀 ) ∈ V )
12 8 9 10 11 fvmptd ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( 0g ‘ 𝑀 ) )