Theorem grpinvcl 18866

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6482  Basecbs 17120  Grpcgrp 18812  inv_gcminusg 18813

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 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-riota 7306  df-ov 7352  df-0g 17345  df-mgm 18514  df-sgrp 18593  df-mnd 18609  df-grp 18815  df-minusg 18816

This theorem is referenced by:  grpinvcld  18867  grprinv  18869  grpinvid1  18870  grpinvid2  18871  grplrinv  18875  grplcan  18879  grpasscan1  18880  grpasscan2  18881  grpinvinv  18884  grpinvcnv  18885  grpinvnzcl  18890  grpsubinv  18891  grplmulf1o  18892  grpinvssd  18896  grpinvadd  18897  grpsubf  18898  grpsubrcan  18900  grpinvsub  18901  grpinvval2  18902  grpsubeq0  18905  grpsubadd  18907  grpaddsubass  18909  grpnpcan  18911  dfgrp3  18918  grplactcnv  18922  grpsubpropd2  18925  prdsinvlem  18928  pwssub  18933  imasgrp  18935  ghmgrp  18945  mulgcl  18970  mulgaddcomlem  18976  mulginvcom  18978  mulginvinv  18979  mulgneg2  18987  subginv  19012  subginvcl  19014  issubg4  19024  grpissubg  19025  isnsg3  19039  subgacs  19040  nmzsubg  19044  eqglact  19058  eqgcpbl  19061  qusgrp  19065  qusinv  19069  qussub  19070  eqg0subg  19075  ghminv  19102  ghmsub  19103  ghmrn  19108  ghmpreima  19117  ghmeql  19118  conjghm  19128  galcan  19183  gacan  19184  gapm  19185  gaorber  19187  gastacl  19188  gastacos  19189  cntzsubg  19218  oppggrp  19236  symgsssg  19346  symgfisg  19347  odinv  19440  sylow2blem1  19499  sylow2blem3  19501  frgpuptf  19649  frgpuplem  19651  ablinvadd  19686  ablsub2inv  19687  ablsub4  19689  ablsubsub4  19697  mulgsubdi  19708  invghm  19712  eqgabl  19713  torsubg  19733  oddvdssubg  19734  cyggeninv  19762  ogrpinv0le  20015  ogrpsub  20016  ogrpaddltbi  20018  ogrpaddltrbid  20020  ogrpinv0lt  20022  ogrpinvlt  20023  ringnegl  20187  ringnegr  20188  ringmneg1  20189  ringmneg2  20190  dvdsrneg  20255  unitinvcl  20275  unitnegcl  20282  cntzsubr  20491  isdrng2  20628  abvneg  20711  abvsubtri  20712  orngsqr  20751  lmodvnegcl  20806  lmodvneg1  20808  lmodvsneg  20809  lmodsubvs  20821  lmodsubdi  20822  lmodsubdir  20823  lssvsubcl  20847  lspsnneg  20909  lmodvsinv  20940  lmodvsinv2  20941  lspexch  21036  lspsolvlem  21049  zrhpsgninv  21492  evpmodpmf1o  21503  dsmmsubg  21650  mplsubglem  21906  mplind  21975  cpmatinvcl  22602  chpscmatgsumbin  22729  chpscmatgsummon  22730  tgplacthmeo  23988  tgpconncomp  23998  qustgpopn  24005  tsmsxplem1  24038  tlmtgp  24081  isngp4  24498  ngpinvds  24499  ngpsubcan  24500  nmtri  24512  ngptgp  24522  tngngp3  24542  ncvspi  25054  deg1suble  26010  deg1sub  26011  dchr2sum  27182  dchrisum0re  27422  symgfcoeu  33025  symgsubg  33030  archirngz  33132  archiabllem1b  33135  archiabllem2c  33138  eqgvscpbl  33288  qusxpid  33301  linds2eq  33319  quslsm  33343  nsgmgclem  33349  ressply1sub  33506  madjusmdetlem3  33802  madjusmdetlem4  33803  lflsub  39056  lflnegcl  39064  ldualvsubcl  39145  ldualvsubval  39146  dvhgrp  41096  lcfrlem2  41532  lcdvsubval  41607  mapdpglem30  41691  baerlem3lem1  41696  baerlem5alem1  41697  baerlem5blem1  41698  baerlem5blem2  41701  fldhmf1  42073  nelsubginvcld  42479  invginvrid  48361  lincext1  48449  lindslinindimp2lem1  48453  ldepsprlem  48467  ldepspr  48468  lincresunit3lem3  48469  lincresunit3lem1  48474  lincresunit3lem2  48475  lincresunit3  48476