Theorem grpinvcl 18908

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ‘cfv 6542  Basecbs 17148  Grpcgrp 18855  inv_gcminusg 18856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-riota 7367  df-ov 7414  df-0g 17391  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18858  df-minusg 18859

This theorem is referenced by:  grpinvcld  18909  grprinv  18911  grpinvid1  18912  grpinvid2  18913  grplrinv  18917  grplcan  18921  grpasscan1  18922  grpasscan2  18923  grpinvinv  18926  grpinvcnv  18927  grpinvnzcl  18931  grpsubinv  18932  grplmulf1o  18933  grpinvssd  18936  grpinvadd  18937  grpsubf  18938  grpsubrcan  18940  grpinvsub  18941  grpinvval2  18942  grpsubeq0  18945  grpsubadd  18947  grpaddsubass  18949  grpnpcan  18951  dfgrp3  18958  grplactcnv  18962  grpsubpropd2  18965  prdsinvlem  18968  pwssub  18973  imasgrp  18975  ghmgrp  18985  mulgcl  19007  mulgaddcomlem  19013  mulginvcom  19015  mulginvinv  19016  mulgneg2  19024  subginv  19049  subginvcl  19051  issubg4  19061  grpissubg  19062  isnsg3  19076  subgacs  19077  nmzsubg  19081  eqglact  19095  eqgcpbl  19098  qusgrp  19101  qusinv  19105  qussub  19106  eqg0subg  19111  ghminv  19137  ghmsub  19138  ghmrn  19143  ghmpreima  19152  ghmeql  19153  conjghm  19163  conjnmz  19166  galcan  19209  gacan  19210  gapm  19211  gaorber  19213  gastacl  19214  gastacos  19215  cntzsubg  19244  oppggrp  19265  symgsssg  19376  symgfisg  19377  odinv  19470  sylow2blem1  19529  sylow2blem3  19531  frgpuptf  19679  frgpuplem  19681  ablinvadd  19716  ablsub2inv  19717  ablsub4  19719  ablsubsub4  19727  mulgsubdi  19738  invghm  19742  eqgabl  19743  torsubg  19763  oddvdssubg  19764  cyggeninv  19792  ringnegl  20190  ringnegr  20191  ringmneg1  20192  ringmneg2  20193  dvdsrneg  20261  unitinvcl  20281  unitnegcl  20288  cntzsubr  20496  isdrng2  20514  abvneg  20585  abvsubtri  20586  lmodvnegcl  20657  lmodvneg1  20659  lmodvsneg  20660  lmodsubvs  20672  lmodsubdi  20673  lmodsubdir  20674  lssvsubcl  20698  lspsnneg  20761  lmodvsinv  20791  lmodvsinv2  20792  lspexch  20887  lspsolvlem  20900  zrhpsgninv  21357  evpmodpmf1o  21368  dsmmsubg  21517  mplsubglem  21777  mplind  21850  mhpinvcl  21914  cpmatinvcl  22439  chpscmatgsumbin  22566  chpscmatgsummon  22567  tgplacthmeo  23827  tgpconncomp  23837  qustgpopn  23844  tsmsxplem1  23877  tlmtgp  23920  isngp4  24341  ngpinvds  24342  ngpsubcan  24343  nmtri  24355  ngptgp  24365  tngngp3  24393  ncvspi  24904  deg1suble  25860  deg1sub  25861  dchr2sum  27012  dchrisum0re  27252  ogrpinv0le  32503  ogrpsub  32504  ogrpaddltbi  32506  ogrpaddltrbid  32508  ogrpinv0lt  32510  ogrpinvlt  32511  symgfcoeu  32513  symgsubg  32518  archirngz  32605  archiabllem1b  32608  archiabllem2c  32611  orngsqr  32692  eqgvscpbl  32735  qusxpid  32749  linds2eq  32771  quslsm  32790  nsgmgclem  32796  ressply1sub  32933  madjusmdetlem3  33107  madjusmdetlem4  33108  lflsub  38240  lflnegcl  38248  ldualvsubcl  38329  ldualvsubval  38330  dvhgrp  40281  lcfrlem2  40717  lcdvsubval  40792  mapdpglem30  40876  baerlem3lem1  40881  baerlem5alem1  40882  baerlem5blem1  40883  baerlem5blem2  40886  fldhmf1  41261  nelsubginvcld  41376  invginvrid  47131  lincext1  47222  lindslinindimp2lem1  47226  ldepsprlem  47240  ldepspr  47241  lincresunit3lem3  47242  lincresunit3lem1  47247  lincresunit3lem2  47248  lincresunit3  47249