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

Metamath Proof Explorer

Theorem mndidcl

Description: The identity element of a monoid belongs to the monoid. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses mndidcl.b ⊢ B = Base G
mndidcl.o ⊢ 0 ˙ = 0 G
Assertion mndidcl ⊢ G ∈ Mnd → 0 ˙ ∈ B

Proof

Step Hyp Ref Expression
1 mndidcl.b ⊢ B = Base G
2 mndidcl.o ⊢ 0 ˙ = 0 G
3 eqid ⊢ + G = + G
4 1 3 mndid ⊢ G ∈ Mnd → ∃ x ∈ B ∀ y ∈ B x + G y = y ∧ y + G x = y
5 1 2 3 4 mgmidcl ⊢ G ∈ Mnd → 0 ˙ ∈ B