Theorem grpinvcl 18948

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ‘cfv 6547  Basecbs 17179  Grpcgrp 18894  inv_gcminusg 18895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-fv 6555  df-riota 7373  df-ov 7420  df-0g 17422  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18897  df-minusg 18898

This theorem is referenced by:  grpinvcld  18949  grprinv  18951  grpinvid1  18952  grpinvid2  18953  grplrinv  18957  grplcan  18961  grpasscan1  18962  grpasscan2  18963  grpinvinv  18966  grpinvcnv  18967  grpinvnzcl  18971  grpsubinv  18972  grplmulf1o  18973  grpinvssd  18977  grpinvadd  18978  grpsubf  18979  grpsubrcan  18981  grpinvsub  18982  grpinvval2  18983  grpsubeq0  18986  grpsubadd  18988  grpaddsubass  18990  grpnpcan  18992  dfgrp3  18999  grplactcnv  19003  grpsubpropd2  19006  prdsinvlem  19009  pwssub  19014  imasgrp  19016  ghmgrp  19026  mulgcl  19050  mulgaddcomlem  19056  mulginvcom  19058  mulginvinv  19059  mulgneg2  19067  subginv  19092  subginvcl  19094  issubg4  19104  grpissubg  19105  isnsg3  19119  subgacs  19120  nmzsubg  19124  eqglact  19138  eqgcpbl  19141  qusgrp  19145  qusinv  19149  qussub  19150  eqg0subg  19155  ghminv  19181  ghmsub  19182  ghmrn  19187  ghmpreima  19196  ghmeql  19197  conjghm  19207  galcan  19259  gacan  19260  gapm  19261  gaorber  19263  gastacl  19264  gastacos  19265  cntzsubg  19294  oppggrp  19315  symgsssg  19426  symgfisg  19427  odinv  19520  sylow2blem1  19579  sylow2blem3  19581  frgpuptf  19729  frgpuplem  19731  ablinvadd  19766  ablsub2inv  19767  ablsub4  19769  ablsubsub4  19777  mulgsubdi  19788  invghm  19792  eqgabl  19793  torsubg  19813  oddvdssubg  19814  cyggeninv  19842  ringnegl  20242  ringnegr  20243  ringmneg1  20244  ringmneg2  20245  dvdsrneg  20313  unitinvcl  20333  unitnegcl  20340  cntzsubr  20549  isdrng2  20642  abvneg  20718  abvsubtri  20719  lmodvnegcl  20790  lmodvneg1  20792  lmodvsneg  20793  lmodsubvs  20805  lmodsubdi  20806  lmodsubdir  20807  lssvsubcl  20832  lspsnneg  20894  lmodvsinv  20925  lmodvsinv2  20926  lspexch  21021  lspsolvlem  21034  zrhpsgninv  21521  evpmodpmf1o  21532  dsmmsubg  21681  mplsubglem  21948  mplind  22021  mhpinvcl  22084  cpmatinvcl  22649  chpscmatgsumbin  22776  chpscmatgsummon  22777  tgplacthmeo  24037  tgpconncomp  24047  qustgpopn  24054  tsmsxplem1  24087  tlmtgp  24130  isngp4  24551  ngpinvds  24552  ngpsubcan  24553  nmtri  24565  ngptgp  24575  tngngp3  24603  ncvspi  25114  deg1suble  26073  deg1sub  26074  dchr2sum  27236  dchrisum0re  27476  ogrpinv0le  32852  ogrpsub  32853  ogrpaddltbi  32855  ogrpaddltrbid  32857  ogrpinv0lt  32859  ogrpinvlt  32860  symgfcoeu  32862  symgsubg  32867  archirngz  32954  archiabllem1b  32957  archiabllem2c  32960  orngsqr  33079  eqgvscpbl  33122  qusxpid  33135  linds2eq  33158  quslsm  33177  nsgmgclem  33183  ressply1sub  33325  madjusmdetlem3  33500  madjusmdetlem4  33501  lflsub  38608  lflnegcl  38616  ldualvsubcl  38697  ldualvsubval  38698  dvhgrp  40649  lcfrlem2  41085  lcdvsubval  41160  mapdpglem30  41244  baerlem3lem1  41249  baerlem5alem1  41250  baerlem5blem1  41251  baerlem5blem2  41254  fldhmf1  41630  nelsubginvcld  41804  invginvrid  47543  lincext1  47634  lindslinindimp2lem1  47638  ldepsprlem  47652  ldepspr  47653  lincresunit3lem3  47654  lincresunit3lem1  47659  lincresunit3lem2  47660  lincresunit3  47661