Theorem mndidcl 18315

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  Basecbs 16840  +_gcplusg 16888  0_gc0g 17067  Mndcmnd 18300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-riota 7212  df-ov 7258  df-0g 17069  df-mgm 18241  df-sgrp 18290  df-mnd 18301

This theorem is referenced by:  mndbn0  18316  hashfinmndnn  18317  mndpfo  18323  prdsidlem  18332  imasmnd  18338  idmhm  18354  mhmf1o  18355  issubmd  18360  submid  18364  0subm  18371  0mhm  18373  mhmco  18377  mhmeql  18379  submacs  18380  mndind  18381  prdspjmhm  18382  pwsdiagmhm  18384  pwsco1mhm  18385  pwsco2mhm  18386  gsumvallem2  18387  dfgrp2  18519  grpidcl  18522  mhmid  18611  mhmmnd  18612  mulgnn0cl  18635  mulgnn0z  18645  cntzsubm  18857  oppgmnd  18876  gex1  19111  mulgnn0di  19342  mulgmhm  19344  subcmn  19353  gsumval3  19423  gsumzcl2  19426  gsumzaddlem  19437  gsumzsplit  19443  gsumzmhm  19453  gsummpt1n0  19481  simpgnideld  19617  srgidcl  19669  srg0cl  19670  ringidcl  19722  gsummgp0  19762  pwssplit1  20236  dsmm0cl  20857  dsmmacl  20858  mndvlid  21452  mndvrid  21453  mdet0  21663  mndifsplit  21693  gsummatr01lem3  21714  pmatcollpw3fi1lem1  21843  tmdmulg  23151  tmdgsum  23154  tsms0  23201  tsmssplit  23211  tsmsxp  23214  cntzsnid  31223  submomnd  31238  omndmul2  31240  omndmul3  31241  omndmul  31242  ogrpinv0le  31243  gsumle  31252  slmd0vcl  31376  sibf0  32201  sitmcl  32218  pwssplit4  40830  c0mgm  45355  c0mhm  45356  c0snmgmhm  45360  c0snmhm  45361  mgpsumz  45586  mndpsuppss  45595  lco0  45656  mndtccatid  46260