Theorem grpinvcl 19054

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ‘cfv 6537  Basecbs 17269  Grpcgrp 19000  inv_gcminusg 19001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-riota 7368  df-ov 7414  df-0g 17494  df-mgm 18698  df-sgrp 18777  df-mnd 18793  df-grp 19003  df-minusg 19004

This theorem is referenced by:  grpinvcld  19055  grprinv  19057  grpinvid1  19058  grpinvid2  19059  grplrinv  19063  grplcan  19067  grpasscan1  19068  grpasscan2  19069  grpinvinv  19072  grpinvcnv  19073  grpinvnzcl  19077  grpsubinv  19078  grplmulf1o  19079  grpinvssd  19083  grpinvadd  19084  grpsubf  19085  grpsubrcan  19087  grpinvsub  19088  grpinvval2  19089  grpsubeq0  19092  grpsubadd  19094  grpaddsubass  19096  grpnpcan  19098  dfgrp3  19105  grplactcnv  19109  grpsubpropd2  19112  prdsinvlem  19115  pwssub  19120  imasgrp  19122  ghmgrp  19132  mulgcl  19157  mulgaddcomlem  19163  mulginvcom  19165  mulginvinv  19166  mulgneg2  19174  subginv  19199  subginvcl  19201  issubg4  19212  grpissubg  19213  isnsg3  19226  subgacs  19227  nmzsubg  19231  eqglact  19247  eqgcpbl  19250  qusxpid  19251  qusgrp  19257  qusinv  19261  qussub  19262  eqg0subg  19267  ghminv  19293  ghmsub  19294  ghmrn  19299  ghmpreima  19308  ghmeql  19309  conjghm  19319  galcan  19374  gacan  19375  gapm  19376  gaorber  19378  gastacl  19379  gastacos  19380  cntzsubg  19409  oppggrp  19427  symgsssg  19537  symgfisg  19538  odinv  19631  sylow2blem1  19690  sylow2blem3  19692  frgpuptf  19840  frgpuplem  19842  ablinvadd  19877  ablsub2inv  19878  ablsub4  19880  ablsubsub4  19888  mulgsubdi  19899  invghm  19903  eqgabl  19904  torsubg  19924  oddvdssubg  19925  cyggeninv  19953  ogrpinv0le  20206  ogrpsub  20207  ogrpaddltbi  20209  ogrpaddltrbid  20211  ogrpinv0lt  20213  ogrpinvlt  20214  ringnegl  20385  ringnegr  20386  ringmneg1  20387  ringmneg2  20388  dvdsrneg  20452  unitinvcl  20472  unitnegcl  20479  cntzsubr  20691  isdrng2  20827  abvneg  20907  abvsubtri  20908  orngsqr  20947  lmodvnegcl  21002  lmodvneg1  21004  lmodvsneg  21005  lmodsubvs  21017  lmodsubdi  21018  lmodsubdir  21019  lssvsubcl  21043  lspsnneg  21105  lmodvsinv  21135  lmodvsinv2  21136  lspexch  21231  lspsolvlem  21244  zrhpsgninv  21704  evpmodpmf1o  21715  dsmmsubg  21862  mplsubglem  22117  mplind  22190  cpmatinvcl  22843  chpscmatgsumbin  22970  chpscmatgsummon  22971  tgplacthmeo  24229  tgpconncomp  24239  qustgpopn  24246  tsmsxplem1  24279  tlmtgp  24322  isngp4  24738  ngpinvds  24739  ngpsubcan  24740  nmtri  24752  ngptgp  24762  tngngp3  24782  ncvspi  25284  deg1suble  26233  deg1sub  26234  dchr2sum  27403  dchrisum0re  27643  symgfcoeu  33343  symgsubg  33348  archirngz  33450  archiabllem1b  33453  archiabllem2c  33456  eqgvscpbl  33613  linds2eq  33638  quslsm  33658  nsgmgclem  33664  ressply1sub  33805  madjusmdetlem3  34164  madjusmdetlem4  34165  lflsub  39765  lflnegcl  39773  ldualvsubcl  39854  ldualvsubval  39855  dvhgrp  41805  lcfrlem2  42241  lcdvsubval  42316  mapdpglem30  42400  baerlem3lem1  42405  baerlem5alem1  42406  baerlem5blem1  42407  baerlem5blem2  42410  fldhmf1  42781  nelsubginvcld  43194  invginvrid  49066  lincext1  49153  lindslinindimp2lem1  49157  ldepsprlem  49171  ldepspr  49172  lincresunit3lem3  49173  lincresunit3lem1  49178  lincresunit3lem2  49179  lincresunit3  49180