Theorem grpinvcl 18957

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  Basecbs 17173  Grpcgrp 18903  inv_gcminusg 18904

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 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

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 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-riota 7318  df-ov 7364  df-0g 17398  df-mgm 18602  df-sgrp 18681  df-mnd 18697  df-grp 18906  df-minusg 18907

This theorem is referenced by:  grpinvcld  18958  grprinv  18960  grpinvid1  18961  grpinvid2  18962  grplrinv  18966  grplcan  18970  grpasscan1  18971  grpasscan2  18972  grpinvinv  18975  grpinvcnv  18976  grpinvnzcl  18981  grpsubinv  18982  grplmulf1o  18983  grpinvssd  18987  grpinvadd  18988  grpsubf  18989  grpsubrcan  18991  grpinvsub  18992  grpinvval2  18993  grpsubeq0  18996  grpsubadd  18998  grpaddsubass  19000  grpnpcan  19002  dfgrp3  19009  grplactcnv  19013  grpsubpropd2  19016  prdsinvlem  19019  pwssub  19024  imasgrp  19026  ghmgrp  19036  mulgcl  19061  mulgaddcomlem  19067  mulginvcom  19069  mulginvinv  19070  mulgneg2  19078  subginv  19103  subginvcl  19105  issubg4  19115  grpissubg  19116  isnsg3  19129  subgacs  19130  nmzsubg  19134  eqglact  19148  eqgcpbl  19151  qusgrp  19155  qusinv  19159  qussub  19160  eqg0subg  19165  ghminv  19192  ghmsub  19193  ghmrn  19198  ghmpreima  19207  ghmeql  19208  conjghm  19218  galcan  19273  gacan  19274  gapm  19275  gaorber  19277  gastacl  19278  gastacos  19279  cntzsubg  19308  oppggrp  19326  symgsssg  19436  symgfisg  19437  odinv  19530  sylow2blem1  19589  sylow2blem3  19591  frgpuptf  19739  frgpuplem  19741  ablinvadd  19776  ablsub2inv  19777  ablsub4  19779  ablsubsub4  19787  mulgsubdi  19798  invghm  19802  eqgabl  19803  torsubg  19823  oddvdssubg  19824  cyggeninv  19852  ogrpinv0le  20105  ogrpsub  20106  ogrpaddltbi  20108  ogrpaddltrbid  20110  ogrpinv0lt  20112  ogrpinvlt  20113  ringnegl  20277  ringnegr  20278  ringmneg1  20279  ringmneg2  20280  dvdsrneg  20344  unitinvcl  20364  unitnegcl  20371  cntzsubr  20577  isdrng2  20714  abvneg  20797  abvsubtri  20798  orngsqr  20837  lmodvnegcl  20892  lmodvneg1  20894  lmodvsneg  20895  lmodsubvs  20907  lmodsubdi  20908  lmodsubdir  20909  lssvsubcl  20933  lspsnneg  20995  lmodvsinv  21026  lmodvsinv2  21027  lspexch  21122  lspsolvlem  21135  zrhpsgninv  21578  evpmodpmf1o  21589  dsmmsubg  21736  mplsubglem  21990  mplind  22061  cpmatinvcl  22695  chpscmatgsumbin  22822  chpscmatgsummon  22823  tgplacthmeo  24081  tgpconncomp  24091  qustgpopn  24098  tsmsxplem1  24131  tlmtgp  24174  isngp4  24590  ngpinvds  24591  ngpsubcan  24592  nmtri  24604  ngptgp  24614  tngngp3  24634  ncvspi  25136  deg1suble  26085  deg1sub  26086  dchr2sum  27253  dchrisum0re  27493  symgfcoeu  33161  symgsubg  33166  archirngz  33268  archiabllem1b  33271  archiabllem2c  33274  eqgvscpbl  33428  qusxpid  33441  linds2eq  33459  quslsm  33483  nsgmgclem  33489  ressply1sub  33648  madjusmdetlem3  33992  madjusmdetlem4  33993  lflsub  39530  lflnegcl  39538  ldualvsubcl  39619  ldualvsubval  39620  dvhgrp  41570  lcfrlem2  42006  lcdvsubval  42081  mapdpglem30  42165  baerlem3lem1  42170  baerlem5alem1  42171  baerlem5blem1  42172  baerlem5blem2  42175  fldhmf1  42546  nelsubginvcld  42958  invginvrid  48858  lincext1  48945  lindslinindimp2lem1  48949  ldepsprlem  48963  ldepspr  48964  lincresunit3lem3  48965  lincresunit3lem1  48970  lincresunit3lem2  48971  lincresunit3  48972