Theorem grpinvcl 18925

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6513  Basecbs 17185  Grpcgrp 18871  inv_gcminusg 18872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-fv 6521  df-riota 7346  df-ov 7392  df-0g 17410  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-grp 18874  df-minusg 18875

This theorem is referenced by:  grpinvcld  18926  grprinv  18928  grpinvid1  18929  grpinvid2  18930  grplrinv  18934  grplcan  18938  grpasscan1  18939  grpasscan2  18940  grpinvinv  18943  grpinvcnv  18944  grpinvnzcl  18949  grpsubinv  18950  grplmulf1o  18951  grpinvssd  18955  grpinvadd  18956  grpsubf  18957  grpsubrcan  18959  grpinvsub  18960  grpinvval2  18961  grpsubeq0  18964  grpsubadd  18966  grpaddsubass  18968  grpnpcan  18970  dfgrp3  18977  grplactcnv  18981  grpsubpropd2  18984  prdsinvlem  18987  pwssub  18992  imasgrp  18994  ghmgrp  19004  mulgcl  19029  mulgaddcomlem  19035  mulginvcom  19037  mulginvinv  19038  mulgneg2  19046  subginv  19071  subginvcl  19073  issubg4  19083  grpissubg  19084  isnsg3  19098  subgacs  19099  nmzsubg  19103  eqglact  19117  eqgcpbl  19120  qusgrp  19124  qusinv  19128  qussub  19129  eqg0subg  19134  ghminv  19161  ghmsub  19162  ghmrn  19167  ghmpreima  19176  ghmeql  19177  conjghm  19187  galcan  19242  gacan  19243  gapm  19244  gaorber  19246  gastacl  19247  gastacos  19248  cntzsubg  19277  oppggrp  19295  symgsssg  19403  symgfisg  19404  odinv  19497  sylow2blem1  19556  sylow2blem3  19558  frgpuptf  19706  frgpuplem  19708  ablinvadd  19743  ablsub2inv  19744  ablsub4  19746  ablsubsub4  19754  mulgsubdi  19765  invghm  19769  eqgabl  19770  torsubg  19790  oddvdssubg  19791  cyggeninv  19819  ringnegl  20217  ringnegr  20218  ringmneg1  20219  ringmneg2  20220  dvdsrneg  20285  unitinvcl  20305  unitnegcl  20312  cntzsubr  20521  isdrng2  20658  abvneg  20741  abvsubtri  20742  lmodvnegcl  20815  lmodvneg1  20817  lmodvsneg  20818  lmodsubvs  20830  lmodsubdi  20831  lmodsubdir  20832  lssvsubcl  20856  lspsnneg  20918  lmodvsinv  20949  lmodvsinv2  20950  lspexch  21045  lspsolvlem  21058  zrhpsgninv  21500  evpmodpmf1o  21511  dsmmsubg  21658  mplsubglem  21914  mplind  21983  cpmatinvcl  22610  chpscmatgsumbin  22737  chpscmatgsummon  22738  tgplacthmeo  23996  tgpconncomp  24006  qustgpopn  24013  tsmsxplem1  24046  tlmtgp  24089  isngp4  24506  ngpinvds  24507  ngpsubcan  24508  nmtri  24520  ngptgp  24530  tngngp3  24550  ncvspi  25062  deg1suble  26018  deg1sub  26019  dchr2sum  27190  dchrisum0re  27430  ogrpinv0le  33035  ogrpsub  33036  ogrpaddltbi  33038  ogrpaddltrbid  33040  ogrpinv0lt  33042  ogrpinvlt  33043  symgfcoeu  33045  symgsubg  33050  archirngz  33149  archiabllem1b  33152  archiabllem2c  33155  orngsqr  33288  eqgvscpbl  33327  qusxpid  33340  linds2eq  33358  quslsm  33382  nsgmgclem  33388  ressply1sub  33545  madjusmdetlem3  33825  madjusmdetlem4  33826  lflsub  39055  lflnegcl  39063  ldualvsubcl  39144  ldualvsubval  39145  dvhgrp  41096  lcfrlem2  41532  lcdvsubval  41607  mapdpglem30  41691  baerlem3lem1  41696  baerlem5alem1  41697  baerlem5blem1  41698  baerlem5blem2  41701  fldhmf1  42073  nelsubginvcld  42477  invginvrid  48345  lincext1  48433  lindslinindimp2lem1  48437  ldepsprlem  48451  ldepspr  48452  lincresunit3lem3  48453  lincresunit3lem1  48458  lincresunit3lem2  48459  lincresunit3  48460