Theorem grpinvcl 19022

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2103  ‘cfv 6572  Basecbs 17253  Grpcgrp 18968  inv_gcminusg 18969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pow 5386  ax-pr 5450  ax-un 7766

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-fv 6580  df-riota 7401  df-ov 7448  df-0g 17496  df-mgm 18673  df-sgrp 18752  df-mnd 18768  df-grp 18971  df-minusg 18972

This theorem is referenced by:  grpinvcld  19023  grprinv  19025  grpinvid1  19026  grpinvid2  19027  grplrinv  19031  grplcan  19035  grpasscan1  19036  grpasscan2  19037  grpinvinv  19040  grpinvcnv  19041  grpinvnzcl  19046  grpsubinv  19047  grplmulf1o  19048  grpinvssd  19052  grpinvadd  19053  grpsubf  19054  grpsubrcan  19056  grpinvsub  19057  grpinvval2  19058  grpsubeq0  19061  grpsubadd  19063  grpaddsubass  19065  grpnpcan  19067  dfgrp3  19074  grplactcnv  19078  grpsubpropd2  19081  prdsinvlem  19084  pwssub  19089  imasgrp  19091  ghmgrp  19101  mulgcl  19126  mulgaddcomlem  19132  mulginvcom  19134  mulginvinv  19135  mulgneg2  19143  subginv  19168  subginvcl  19170  issubg4  19180  grpissubg  19181  isnsg3  19195  subgacs  19196  nmzsubg  19200  eqglact  19214  eqgcpbl  19217  qusgrp  19221  qusinv  19225  qussub  19226  eqg0subg  19231  ghminv  19258  ghmsub  19259  ghmrn  19264  ghmpreima  19273  ghmeql  19274  conjghm  19284  galcan  19339  gacan  19340  gapm  19341  gaorber  19343  gastacl  19344  gastacos  19345  cntzsubg  19374  oppggrp  19395  symgsssg  19504  symgfisg  19505  odinv  19598  sylow2blem1  19657  sylow2blem3  19659  frgpuptf  19807  frgpuplem  19809  ablinvadd  19844  ablsub2inv  19845  ablsub4  19847  ablsubsub4  19855  mulgsubdi  19866  invghm  19870  eqgabl  19871  torsubg  19891  oddvdssubg  19892  cyggeninv  19920  ringnegl  20320  ringnegr  20321  ringmneg1  20322  ringmneg2  20323  dvdsrneg  20391  unitinvcl  20411  unitnegcl  20418  cntzsubr  20629  isdrng2  20760  abvneg  20844  abvsubtri  20845  lmodvnegcl  20918  lmodvneg1  20920  lmodvsneg  20921  lmodsubvs  20933  lmodsubdi  20934  lmodsubdir  20935  lssvsubcl  20960  lspsnneg  21022  lmodvsinv  21053  lmodvsinv2  21054  lspexch  21149  lspsolvlem  21162  zrhpsgninv  21621  evpmodpmf1o  21632  dsmmsubg  21781  mplsubglem  22036  mplind  22111  mhpinvcl  22172  cpmatinvcl  22737  chpscmatgsumbin  22864  chpscmatgsummon  22865  tgplacthmeo  24125  tgpconncomp  24135  qustgpopn  24142  tsmsxplem1  24175  tlmtgp  24218  isngp4  24639  ngpinvds  24640  ngpsubcan  24641  nmtri  24653  ngptgp  24663  tngngp3  24691  ncvspi  25202  deg1suble  26158  deg1sub  26159  dchr2sum  27326  dchrisum0re  27566  ogrpinv0le  33057  ogrpsub  33058  ogrpaddltbi  33060  ogrpaddltrbid  33062  ogrpinv0lt  33064  ogrpinvlt  33065  symgfcoeu  33067  symgsubg  33072  archirngz  33161  archiabllem1b  33164  archiabllem2c  33167  orngsqr  33291  eqgvscpbl  33335  qusxpid  33348  linds2eq  33366  quslsm  33390  nsgmgclem  33396  ressply1sub  33552  madjusmdetlem3  33767  madjusmdetlem4  33768  lflsub  38971  lflnegcl  38979  ldualvsubcl  39060  ldualvsubval  39061  dvhgrp  41012  lcfrlem2  41448  lcdvsubval  41523  mapdpglem30  41607  baerlem3lem1  41612  baerlem5alem1  41613  baerlem5blem1  41614  baerlem5blem2  41617  fldhmf1  41995  nelsubginvcld  42384  invginvrid  48010  lincext1  48101  lindslinindimp2lem1  48105  ldepsprlem  48119  ldepspr  48120  lincresunit3lem3  48121  lincresunit3lem1  48126  lincresunit3lem2  48127  lincresunit3  48128