Theorem grpinvcl 18963

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  Basecbs 17179  Grpcgrp 18909  inv_gcminusg 18910

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-riota 7324  df-ov 7370  df-0g 17404  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-grp 18912  df-minusg 18913

This theorem is referenced by:  grpinvcld  18964  grprinv  18966  grpinvid1  18967  grpinvid2  18968  grplrinv  18972  grplcan  18976  grpasscan1  18977  grpasscan2  18978  grpinvinv  18981  grpinvcnv  18982  grpinvnzcl  18987  grpsubinv  18988  grplmulf1o  18989  grpinvssd  18993  grpinvadd  18994  grpsubf  18995  grpsubrcan  18997  grpinvsub  18998  grpinvval2  18999  grpsubeq0  19002  grpsubadd  19004  grpaddsubass  19006  grpnpcan  19008  dfgrp3  19015  grplactcnv  19019  grpsubpropd2  19022  prdsinvlem  19025  pwssub  19030  imasgrp  19032  ghmgrp  19042  mulgcl  19067  mulgaddcomlem  19073  mulginvcom  19075  mulginvinv  19076  mulgneg2  19084  subginv  19109  subginvcl  19111  issubg4  19121  grpissubg  19122  isnsg3  19135  subgacs  19136  nmzsubg  19140  eqglact  19154  eqgcpbl  19157  qusgrp  19161  qusinv  19165  qussub  19166  eqg0subg  19171  ghminv  19198  ghmsub  19199  ghmrn  19204  ghmpreima  19213  ghmeql  19214  conjghm  19224  galcan  19279  gacan  19280  gapm  19281  gaorber  19283  gastacl  19284  gastacos  19285  cntzsubg  19314  oppggrp  19332  symgsssg  19442  symgfisg  19443  odinv  19536  sylow2blem1  19595  sylow2blem3  19597  frgpuptf  19745  frgpuplem  19747  ablinvadd  19782  ablsub2inv  19783  ablsub4  19785  ablsubsub4  19793  mulgsubdi  19804  invghm  19808  eqgabl  19809  torsubg  19829  oddvdssubg  19830  cyggeninv  19858  ogrpinv0le  20111  ogrpsub  20112  ogrpaddltbi  20114  ogrpaddltrbid  20116  ogrpinv0lt  20118  ogrpinvlt  20119  ringnegl  20283  ringnegr  20284  ringmneg1  20285  ringmneg2  20286  dvdsrneg  20350  unitinvcl  20370  unitnegcl  20377  cntzsubr  20583  isdrng2  20720  abvneg  20803  abvsubtri  20804  orngsqr  20843  lmodvnegcl  20898  lmodvneg1  20900  lmodvsneg  20901  lmodsubvs  20913  lmodsubdi  20914  lmodsubdir  20915  lssvsubcl  20939  lspsnneg  21001  lmodvsinv  21031  lmodvsinv2  21032  lspexch  21127  lspsolvlem  21140  zrhpsgninv  21565  evpmodpmf1o  21576  dsmmsubg  21723  mplsubglem  21977  mplind  22048  cpmatinvcl  22682  chpscmatgsumbin  22809  chpscmatgsummon  22810  tgplacthmeo  24068  tgpconncomp  24078  qustgpopn  24085  tsmsxplem1  24118  tlmtgp  24161  isngp4  24577  ngpinvds  24578  ngpsubcan  24579  nmtri  24591  ngptgp  24601  tngngp3  24621  ncvspi  25123  deg1suble  26072  deg1sub  26073  dchr2sum  27236  dchrisum0re  27476  symgfcoeu  33143  symgsubg  33148  archirngz  33250  archiabllem1b  33253  archiabllem2c  33256  eqgvscpbl  33410  qusxpid  33423  linds2eq  33441  quslsm  33465  nsgmgclem  33471  ressply1sub  33630  madjusmdetlem3  33973  madjusmdetlem4  33974  lflsub  39513  lflnegcl  39521  ldualvsubcl  39602  ldualvsubval  39603  dvhgrp  41553  lcfrlem2  41989  lcdvsubval  42064  mapdpglem30  42148  baerlem3lem1  42153  baerlem5alem1  42154  baerlem5blem1  42155  baerlem5blem2  42158  fldhmf1  42529  nelsubginvcld  42941  invginvrid  48843  lincext1  48930  lindslinindimp2lem1  48934  ldepsprlem  48948  ldepspr  48949  lincresunit3lem3  48950  lincresunit3lem1  48955  lincresunit3lem2  48956  lincresunit3  48957