Theorem mndidcl 18640

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 2733	. 2 ⊢ (+g‘𝐺) = (+g‘𝐺)
4	1, 3	mndid 18635	. 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦))
5	1, 2, 3, 4	mgmidcl 18585	1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ‘cfv 6544  Basecbs 17144  +_gcplusg 17197  0_gc0g 17385  Mndcmnd 18625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-riota 7365  df-ov 7412  df-0g 17387  df-mgm 18561  df-sgrp 18610  df-mnd 18626

This theorem is referenced by:  mndbn0  18641  hashfinmndnn  18642  mndpfo  18648  prdsidlem  18657  imasmnd  18663  xpsmnd0  18666  idmhm  18681  mhmf1o  18682  issubmd  18687  submid  18691  0subm  18698  0mhm  18700  mhmco  18704  mhmeql  18707  submacs  18708  mndind  18709  prdspjmhm  18710  pwsdiagmhm  18712  pwsco1mhm  18713  pwsco2mhm  18714  gsumvallem2  18715  dfgrp2  18847  grpidcl  18850  mhmid  18946  mhmmnd  18947  mulgnn0cl  18970  mulgnn0z  18981  cntzsubm  19202  oppgmnd  19221  gex1  19459  mulgnn0di  19693  mulgmhm  19695  subcmn  19705  gsumval3  19775  gsumzcl2  19778  gsumzaddlem  19789  gsumzsplit  19795  gsumzmhm  19805  gsummpt1n0  19833  simpgnideld  19969  srgidcl  20022  srg0cl  20023  ringidcl  20083  gsummgp0  20130  pwssplit1  20670  dsmm0cl  21295  dsmmacl  21296  mndvlid  21895  mndvrid  21896  mdet0  22108  mndifsplit  22138  gsummatr01lem3  22159  pmatcollpw3fi1lem1  22288  tmdmulg  23596  tmdgsum  23599  tsms0  23646  tsmssplit  23656  tsmsxp  23659  cntzsnid  32213  submomnd  32228  omndmul2  32230  omndmul3  32231  omndmul  32232  ogrpinv0le  32233  gsumle  32242  slmd0vcl  32366  ply1degltdimlem  32707  sibf0  33333  sitmcl  33350  mhmcompl  41120  pwssplit4  41831  c0mgm  46708  c0mhm  46709  c0snmgmhm  46713  c0snmhm  46714  rngqiprngimf1  46785  mgpsumz  47038  mndpsuppss  47047  lco0  47108  mndtccatid  47713