Theorem mndidcl 17752

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

Hypotheses

Ref	Expression
mndidcl.b	⊢ 𝐵 = (Base‘𝐺)
mndidcl.o	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
mndidcl	⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

Proof of Theorem mndidcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mndidcl.b	. 2 ⊢ 𝐵 = (Base‘𝐺)
2		mndidcl.o	. 2 ⊢ 0 = (0g‘𝐺)
3		eqid 2795	. 2 ⊢ (+g‘𝐺) = (+g‘𝐺)
4	1, 3	mndid 17747	. 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦))
5	1, 2, 3, 4	mgmidcl 17709	1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081  ‘cfv 6230  Basecbs 16317  +_gcplusg 16399  0_gc0g 16547  Mndcmnd 17738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-iota 6194  df-fun 6232  df-fv 6238  df-riota 6982  df-ov 7024  df-0g 16549  df-mgm 17686  df-sgrp 17728  df-mnd 17739

This theorem is referenced by:  mndpfo  17758  prdsidlem  17766  imasmnd  17772  idmhm  17788  mhmf1o  17789  issubmd  17793  submid  17795  0mhm  17802  mhmco  17806  mhmeql  17808  submacs  17809  mndind  17810  prdspjmhm  17811  pwsdiagmhm  17813  pwsco1mhm  17814  pwsco2mhm  17815  gsumvallem2  17816  dfgrp2  17891  grpidcl  17894  mhmid  17982  mhmmnd  17983  mulgnn0cl  18004  mulgnn0z  18013  cntzsubm  18212  oppgmnd  18228  gex1  18451  mulgnn0di  18676  mulgmhm  18678  subcmn  18687  gsumval3  18753  gsumzcl2  18756  gsumzaddlem  18766  gsumzsplit  18772  gsumzmhm  18782  gsummpt1n0  18810  srgidcl  18963  srg0cl  18964  ringidcl  19013  gsummgp0  19053  pwssplit1  19526  dsmm0cl  20571  dsmmacl  20572  mndvlid  20691  mndvrid  20692  mdet0  20904  mndifsplit  20934  gsummatr01lem3  20955  pmatcollpw3fi1lem1  21083  tmdmulg  22389  tmdgsum  22392  tsms0  22438  tsmssplit  22448  tsmsxp  22451  submomnd  30376  omndmul2  30378  omndmul3  30379  omndmul  30380  ogrpinv0le  30381  slmdbn0  30479  slmdsn0  30482  slmd0vcl  30492  gsumle  30499  cntzsnid  30512  sibf0  31214  sitmcl  31231  pwssplit4  39199  hashfinmndnn  40169  simpgnideld  40180  c0mgm  43684  c0mhm  43685  c0snmgmhm  43689  c0snmhm  43690  mgpsumz  43914  mndpsuppss  43925  lco0  43988