Theorem mndidcl 18188

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110  ‘cfv 6380  Basecbs 16760  +_gcplusg 16802  0_gc0g 16944  Mndcmnd 18173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-iota 6338  df-fun 6382  df-fv 6388  df-riota 7170  df-ov 7216  df-0g 16946  df-mgm 18114  df-sgrp 18163  df-mnd 18174

This theorem is referenced by:  mndbn0  18189  hashfinmndnn  18190  mndpfo  18196  prdsidlem  18205  imasmnd  18211  idmhm  18227  mhmf1o  18228  issubmd  18233  submid  18237  0subm  18244  0mhm  18246  mhmco  18250  mhmeql  18252  submacs  18253  mndind  18254  prdspjmhm  18255  pwsdiagmhm  18257  pwsco1mhm  18258  pwsco2mhm  18259  gsumvallem2  18260  dfgrp2  18392  grpidcl  18395  mhmid  18484  mhmmnd  18485  mulgnn0cl  18508  mulgnn0z  18518  cntzsubm  18730  oppgmnd  18746  gex1  18980  mulgnn0di  19211  mulgmhm  19213  subcmn  19222  gsumval3  19292  gsumzcl2  19295  gsumzaddlem  19306  gsumzsplit  19312  gsumzmhm  19322  gsummpt1n0  19350  simpgnideld  19486  srgidcl  19533  srg0cl  19534  ringidcl  19586  gsummgp0  19626  pwssplit1  20096  dsmm0cl  20702  dsmmacl  20703  mndvlid  21292  mndvrid  21293  mdet0  21503  mndifsplit  21533  gsummatr01lem3  21554  pmatcollpw3fi1lem1  21683  tmdmulg  22989  tmdgsum  22992  tsms0  23039  tsmssplit  23049  tsmsxp  23052  cntzsnid  31040  submomnd  31055  omndmul2  31057  omndmul3  31058  omndmul  31059  ogrpinv0le  31060  gsumle  31069  slmd0vcl  31193  sibf0  32013  sitmcl  32030  pwssplit4  40617  c0mgm  45140  c0mhm  45141  c0snmgmhm  45145  c0snmhm  45146  mgpsumz  45371  mndpsuppss  45380  lco0  45441  mndtccatid  46045