Theorem mndidcl 18840

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  Basecbs 17291  +_gcplusg 17332  0_gc0g 17514  Mndcmnd 18824

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-riota 7376  df-ov 7422  df-0g 17516  df-mgm 18720  df-sgrp 18809  df-mnd 18825

This theorem is used by:  mndbn0  18841  hashfinmndnn  18842  mndpfoOLD  18850  mndpsuppss  18860  prdsidlem  18864  imasmnd  18870  xpsmnd0  18873  idmhm  18890  mhmf1o  18891  mndvlid  18894  mndvrid  18895  issubmd  18901  submid  18905  0subm  18913  0mhm  18915  mhmco  18919  mhmeql  18922  submacs  18923  mndind  18924  prdspjmhm  18925  pwsdiagmhm  18927  pwsco1mhm  18928  pwsco2mhm  18929  gsumvallem2  18930  dfgrp2  19073  grpidcl  19076  mhmid  19173  mhmmnd  19174  mulgnn0cl  19200  mulgnn0z  19211  cntzsubm  19452  oppgmnd  19468  gex1  19705  mulgnn0di  19939  mulgmhm  19941  subcmn  19951  gsumval3  20021  gsumzcl2  20024  gsumzaddlem  20035  gsumzsplit  20041  gsumzmhm  20051  gsummpt1n0  20079  simpgnideld  20215  submomnd  20246  omndmul2  20247  omndmul3  20248  omndmul  20249  ogrpinv0le  20250  gsumle  20259  srgidcl  20325  srg0cl  20326  ringidcl  20393  gsummgp0  20445  c0mgm  20587  c0mhm  20588  c0snmgmhm  20590  c0snmhm  20591  pwssplit1  21230  rngqiprngimf1  21490  dsmm0cl  21940  dsmmacl  21941  mhmcompl  22322  mdet0  22813  mndifsplit  22843  gsummatr01lem3  22864  pmatcollpw3fi1lem1  22993  tmdmulg  24300  tmdgsum  24303  tsms0  24350  tsmssplit  24360  tsmsxp  24363  mndlactfo  33411  mndractfo  33413  mndlactf1o  33414  mndractf1o  33415  suppgsumssiun  33456  gsumwun  33460  cntzsnid  33464  fxpsubm  33556  slmd0vcl  33605  ply1degltdimlem  34076  lvecendof1f1o  34087  sibf0  34789  sitmcl  34806  primrootsunit1  42922  primrootscoprmpow  42924  primrootscoprbij  42927  evl1gprodd  42942  ringexp0nn  42959  aks6d1c5lem2  42963  pwssplit4  43874  mgpsumz  49199  lco0  49264  mndtccatid  50422