Theorem grpinvcl 18954

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ‘cfv 6485  Basecbs 17170  Grpcgrp 18900  inv_gcminusg 18901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-riota 7313  df-ov 7359  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903  df-minusg 18904

This theorem is referenced by:  grpinvcld  18955  grprinv  18957  grpinvid1  18958  grpinvid2  18959  grplrinv  18963  grplcan  18967  grpasscan1  18968  grpasscan2  18969  grpinvinv  18972  grpinvcnv  18973  grpinvnzcl  18978  grpsubinv  18979  grplmulf1o  18980  grpinvssd  18984  grpinvadd  18985  grpsubf  18986  grpsubrcan  18988  grpinvsub  18989  grpinvval2  18990  grpsubeq0  18993  grpsubadd  18995  grpaddsubass  18997  grpnpcan  18999  dfgrp3  19006  grplactcnv  19010  grpsubpropd2  19013  prdsinvlem  19016  pwssub  19021  imasgrp  19023  ghmgrp  19033  mulgcl  19058  mulgaddcomlem  19064  mulginvcom  19066  mulginvinv  19067  mulgneg2  19075  subginv  19100  subginvcl  19102  issubg4  19112  grpissubg  19113  isnsg3  19126  subgacs  19127  nmzsubg  19131  eqglact  19145  eqgcpbl  19148  qusgrp  19152  qusinv  19156  qussub  19157  eqg0subg  19162  ghminv  19189  ghmsub  19190  ghmrn  19195  ghmpreima  19204  ghmeql  19205  conjghm  19215  galcan  19270  gacan  19271  gapm  19272  gaorber  19274  gastacl  19275  gastacos  19276  cntzsubg  19305  oppggrp  19323  symgsssg  19433  symgfisg  19434  odinv  19527  sylow2blem1  19586  sylow2blem3  19588  frgpuptf  19736  frgpuplem  19738  ablinvadd  19773  ablsub2inv  19774  ablsub4  19776  ablsubsub4  19784  mulgsubdi  19795  invghm  19799  eqgabl  19800  torsubg  19820  oddvdssubg  19821  cyggeninv  19849  ogrpinv0le  20102  ogrpsub  20103  ogrpaddltbi  20105  ogrpaddltrbid  20107  ogrpinv0lt  20109  ogrpinvlt  20110  ringnegl  20274  ringnegr  20275  ringmneg1  20276  ringmneg2  20277  dvdsrneg  20341  unitinvcl  20361  unitnegcl  20368  cntzsubr  20578  isdrng2  20715  abvneg  20798  abvsubtri  20799  orngsqr  20838  lmodvnegcl  20893  lmodvneg1  20895  lmodvsneg  20896  lmodsubvs  20908  lmodsubdi  20909  lmodsubdir  20910  lssvsubcl  20934  lspsnneg  20996  lmodvsinv  21026  lmodvsinv2  21027  lspexch  21122  lspsolvlem  21135  zrhpsgninv  21560  evpmodpmf1o  21571  dsmmsubg  21718  mplsubglem  21973  mplind  22046  cpmatinvcl  22700  chpscmatgsumbin  22827  chpscmatgsummon  22828  tgplacthmeo  24086  tgpconncomp  24096  qustgpopn  24103  tsmsxplem1  24136  tlmtgp  24179  isngp4  24595  ngpinvds  24596  ngpsubcan  24597  nmtri  24609  ngptgp  24619  tngngp3  24639  ncvspi  25141  deg1suble  26090  deg1sub  26091  dchr2sum  27254  dchrisum0re  27494  symgfcoeu  33163  symgsubg  33168  archirngz  33270  archiabllem1b  33273  archiabllem2c  33276  eqgvscpbl  33433  qusxpid  33446  linds2eq  33464  quslsm  33488  nsgmgclem  33494  ressply1sub  33653  madjusmdetlem3  34013  madjusmdetlem4  34014  lflsub  39559  lflnegcl  39567  ldualvsubcl  39648  ldualvsubval  39649  dvhgrp  41599  lcfrlem2  42035  lcdvsubval  42110  mapdpglem30  42194  baerlem3lem1  42199  baerlem5alem1  42200  baerlem5blem1  42201  baerlem5blem2  42204  fldhmf1  42575  nelsubginvcld  42986  invginvrid  48858  lincext1  48945  lindslinindimp2lem1  48949  ldepsprlem  48963  ldepspr  48964  lincresunit3lem3  48965  lincresunit3lem1  48970  lincresunit3lem2  48971  lincresunit3  48972