Theorem grpinvcl 18932

Description: A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.)

Hypotheses

Ref	Expression
grpinvcl.b	⊢ 𝐵 = (Base‘𝐺)
grpinvcl.n	⊢ 𝑁 = (invg‘𝐺)

Assertion

Ref	Expression
grpinvcl	⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵)

Proof of Theorem grpinvcl

Step	Hyp	Ref	Expression
1		grpinvcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
2		grpinvcl.n	. . 3 ⊢ 𝑁 = (invg‘𝐺)
3	1, 2	grpinvf 18931	. 2 ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵)
4	3	ffvelcdmda 7038	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  Basecbs 17148  Grpcgrp 18878  inv_gcminusg 18879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-riota 7325  df-ov 7371  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18881  df-minusg 18882

This theorem is referenced by:  grpinvcld  18933  grprinv  18935  grpinvid1  18936  grpinvid2  18937  grplrinv  18941  grplcan  18945  grpasscan1  18946  grpasscan2  18947  grpinvinv  18950  grpinvcnv  18951  grpinvnzcl  18956  grpsubinv  18957  grplmulf1o  18958  grpinvssd  18962  grpinvadd  18963  grpsubf  18964  grpsubrcan  18966  grpinvsub  18967  grpinvval2  18968  grpsubeq0  18971  grpsubadd  18973  grpaddsubass  18975  grpnpcan  18977  dfgrp3  18984  grplactcnv  18988  grpsubpropd2  18991  prdsinvlem  18994  pwssub  18999  imasgrp  19001  ghmgrp  19011  mulgcl  19036  mulgaddcomlem  19042  mulginvcom  19044  mulginvinv  19045  mulgneg2  19053  subginv  19078  subginvcl  19080  issubg4  19090  grpissubg  19091  isnsg3  19104  subgacs  19105  nmzsubg  19109  eqglact  19123  eqgcpbl  19126  qusgrp  19130  qusinv  19134  qussub  19135  eqg0subg  19140  ghminv  19167  ghmsub  19168  ghmrn  19173  ghmpreima  19182  ghmeql  19183  conjghm  19193  galcan  19248  gacan  19249  gapm  19250  gaorber  19252  gastacl  19253  gastacos  19254  cntzsubg  19283  oppggrp  19301  symgsssg  19411  symgfisg  19412  odinv  19505  sylow2blem1  19564  sylow2blem3  19566  frgpuptf  19714  frgpuplem  19716  ablinvadd  19751  ablsub2inv  19752  ablsub4  19754  ablsubsub4  19762  mulgsubdi  19773  invghm  19777  eqgabl  19778  torsubg  19798  oddvdssubg  19799  cyggeninv  19827  ogrpinv0le  20080  ogrpsub  20081  ogrpaddltbi  20083  ogrpaddltrbid  20085  ogrpinv0lt  20087  ogrpinvlt  20088  ringnegl  20252  ringnegr  20253  ringmneg1  20254  ringmneg2  20255  dvdsrneg  20321  unitinvcl  20341  unitnegcl  20348  cntzsubr  20554  isdrng2  20691  abvneg  20774  abvsubtri  20775  orngsqr  20814  lmodvnegcl  20869  lmodvneg1  20871  lmodvsneg  20872  lmodsubvs  20884  lmodsubdi  20885  lmodsubdir  20886  lssvsubcl  20910  lspsnneg  20972  lmodvsinv  21003  lmodvsinv2  21004  lspexch  21099  lspsolvlem  21112  zrhpsgninv  21555  evpmodpmf1o  21566  dsmmsubg  21713  mplsubglem  21969  mplind  22040  cpmatinvcl  22676  chpscmatgsumbin  22803  chpscmatgsummon  22804  tgplacthmeo  24062  tgpconncomp  24072  qustgpopn  24079  tsmsxplem1  24112  tlmtgp  24155  isngp4  24571  ngpinvds  24572  ngpsubcan  24573  nmtri  24585  ngptgp  24595  tngngp3  24615  ncvspi  25127  deg1suble  26083  deg1sub  26084  dchr2sum  27255  dchrisum0re  27495  symgfcoeu  33180  symgsubg  33185  archirngz  33287  archiabllem1b  33290  archiabllem2c  33293  eqgvscpbl  33447  qusxpid  33460  linds2eq  33478  quslsm  33502  nsgmgclem  33508  ressply1sub  33667  madjusmdetlem3  34011  madjusmdetlem4  34012  lflsub  39447  lflnegcl  39455  ldualvsubcl  39536  ldualvsubval  39537  dvhgrp  41487  lcfrlem2  41923  lcdvsubval  41998  mapdpglem30  42082  baerlem3lem1  42087  baerlem5alem1  42088  baerlem5blem1  42089  baerlem5blem2  42092  fldhmf1  42464  nelsubginvcld  42870  invginvrid  48731  lincext1  48818  lindslinindimp2lem1  48822  ldepsprlem  48836  ldepspr  48837  lincresunit3lem3  48838  lincresunit3lem1  48843  lincresunit3lem2  48844  lincresunit3  48845