Theorem grpinvcl 18871

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 18870	. 2 ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵)
4	3	ffvelcdmda 7086	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ‘cfv 6543  Basecbs 17143  Grpcgrp 18818  inv_gcminusg 18819

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-riota 7364  df-ov 7411  df-0g 17386  df-mgm 18560  df-sgrp 18609  df-mnd 18625  df-grp 18821  df-minusg 18822

This theorem is referenced by:  grpinvcld  18872  grprinv  18874  grpinvid1  18875  grpinvid2  18876  grplrinv  18880  grplcan  18884  grpasscan1  18885  grpasscan2  18886  grpinvinv  18889  grpinvcnv  18890  grpinvnzcl  18894  grpsubinv  18895  grplmulf1o  18896  grpinvssd  18899  grpinvadd  18900  grpsubf  18901  grpsubrcan  18903  grpinvsub  18904  grpinvval2  18905  grpsubeq0  18908  grpsubadd  18910  grpaddsubass  18912  grpnpcan  18914  dfgrp3  18921  grplactcnv  18925  grpsubpropd2  18928  prdsinvlem  18931  pwssub  18936  imasgrp  18938  ghmgrp  18948  mulgcl  18970  mulgaddcomlem  18976  mulginvcom  18978  mulginvinv  18979  mulgneg2  18987  subginv  19012  subginvcl  19014  issubg4  19024  grpissubg  19025  isnsg3  19039  subgacs  19040  nmzsubg  19044  eqglact  19058  eqgcpbl  19061  qusgrp  19064  qusinv  19068  qussub  19069  eqg0subg  19072  ghminv  19098  ghmsub  19099  ghmrn  19104  ghmpreima  19113  ghmeql  19114  conjghm  19122  conjnmz  19125  galcan  19167  gacan  19168  gapm  19169  gaorber  19171  gastacl  19172  gastacos  19173  cntzsubg  19202  oppggrp  19223  symgsssg  19334  symgfisg  19335  odinv  19428  sylow2blem1  19487  sylow2blem3  19489  frgpuptf  19637  frgpuplem  19639  ablinvadd  19674  ablsub2inv  19675  ablsub4  19677  ablsubsub4  19685  mulgsubdi  19696  invghm  19700  eqgabl  19701  torsubg  19721  oddvdssubg  19722  cyggeninv  19750  ringnegl  20113  ringnegr  20114  ringmneg1  20115  ringmneg2  20116  ringm2neg  20117  ringsubdi  20118  ringsubdir  20119  dvdsrneg  20183  unitinvcl  20203  unitnegcl  20210  cntzsubr  20352  isdrng2  20370  abvneg  20441  abvsubtri  20442  lmodvnegcl  20512  lmodvneg1  20514  lmodvsneg  20515  lmodsubvs  20527  lmodsubdi  20528  lmodsubdir  20529  lssvsubcl  20553  lssvnegcl  20566  lspsnneg  20616  lmodvsinv  20646  lmodvsinv2  20647  lspexch  20741  lspsolvlem  20754  zrhpsgninv  21137  evpmodpmf1o  21148  dsmmsubg  21297  mplsubglem  21557  mplind  21630  mhpinvcl  21694  cpmatinvcl  22218  chpscmatgsumbin  22345  chpscmatgsummon  22346  tgplacthmeo  23606  tgpconncomp  23616  qustgpopn  23623  tsmsxplem1  23656  tlmtgp  23699  isngp4  24120  ngpinvds  24121  ngpsubcan  24122  nmtri  24134  ngptgp  24144  tngngp3  24172  ncvspi  24672  deg1suble  25624  deg1sub  25625  dchr2sum  26773  dchrisum0re  27013  ogrpinv0le  32228  ogrpsub  32229  ogrpaddltbi  32231  ogrpaddltrbid  32233  ogrpinv0lt  32235  ogrpinvlt  32236  symgfcoeu  32238  symgsubg  32243  archirngz  32330  archiabllem1b  32333  archiabllem2c  32336  orngsqr  32417  eqgvscpbl  32460  qusxpid  32470  linds2eq  32492  quslsm  32511  nsgmgclem  32517  ressply1sub  32654  madjusmdetlem3  32804  madjusmdetlem4  32805  lflsub  37932  lflnegcl  37940  ldualvsubcl  38021  ldualvsubval  38022  dvhgrp  39973  lcfrlem2  40409  lcdvsubval  40484  mapdpglem30  40568  baerlem3lem1  40573  baerlem5alem1  40574  baerlem5blem1  40575  baerlem5blem2  40578  fldhmf1  40950  nelsubginvcld  41072  invginvrid  47033  lincext1  47125  lindslinindimp2lem1  47129  ldepsprlem  47143  ldepspr  47144  lincresunit3lem3  47145  lincresunit3lem1  47150  lincresunit3lem2  47151  lincresunit3  47152