Theorem grpinvcl 18900

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ‘cfv 6481  Basecbs 17120  Grpcgrp 18846  inv_gcminusg 18847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-riota 7303  df-ov 7349  df-0g 17345  df-mgm 18548  df-sgrp 18627  df-mnd 18643  df-grp 18849  df-minusg 18850

This theorem is referenced by:  grpinvcld  18901  grprinv  18903  grpinvid1  18904  grpinvid2  18905  grplrinv  18909  grplcan  18913  grpasscan1  18914  grpasscan2  18915  grpinvinv  18918  grpinvcnv  18919  grpinvnzcl  18924  grpsubinv  18925  grplmulf1o  18926  grpinvssd  18930  grpinvadd  18931  grpsubf  18932  grpsubrcan  18934  grpinvsub  18935  grpinvval2  18936  grpsubeq0  18939  grpsubadd  18941  grpaddsubass  18943  grpnpcan  18945  dfgrp3  18952  grplactcnv  18956  grpsubpropd2  18959  prdsinvlem  18962  pwssub  18967  imasgrp  18969  ghmgrp  18979  mulgcl  19004  mulgaddcomlem  19010  mulginvcom  19012  mulginvinv  19013  mulgneg2  19021  subginv  19046  subginvcl  19048  issubg4  19058  grpissubg  19059  isnsg3  19072  subgacs  19073  nmzsubg  19077  eqglact  19091  eqgcpbl  19094  qusgrp  19098  qusinv  19102  qussub  19103  eqg0subg  19108  ghminv  19135  ghmsub  19136  ghmrn  19141  ghmpreima  19150  ghmeql  19151  conjghm  19161  galcan  19216  gacan  19217  gapm  19218  gaorber  19220  gastacl  19221  gastacos  19222  cntzsubg  19251  oppggrp  19269  symgsssg  19379  symgfisg  19380  odinv  19473  sylow2blem1  19532  sylow2blem3  19534  frgpuptf  19682  frgpuplem  19684  ablinvadd  19719  ablsub2inv  19720  ablsub4  19722  ablsubsub4  19730  mulgsubdi  19741  invghm  19745  eqgabl  19746  torsubg  19766  oddvdssubg  19767  cyggeninv  19795  ogrpinv0le  20048  ogrpsub  20049  ogrpaddltbi  20051  ogrpaddltrbid  20053  ogrpinv0lt  20055  ogrpinvlt  20056  ringnegl  20220  ringnegr  20221  ringmneg1  20222  ringmneg2  20223  dvdsrneg  20288  unitinvcl  20308  unitnegcl  20315  cntzsubr  20521  isdrng2  20658  abvneg  20741  abvsubtri  20742  orngsqr  20781  lmodvnegcl  20836  lmodvneg1  20838  lmodvsneg  20839  lmodsubvs  20851  lmodsubdi  20852  lmodsubdir  20853  lssvsubcl  20877  lspsnneg  20939  lmodvsinv  20970  lmodvsinv2  20971  lspexch  21066  lspsolvlem  21079  zrhpsgninv  21522  evpmodpmf1o  21533  dsmmsubg  21680  mplsubglem  21936  mplind  22005  cpmatinvcl  22632  chpscmatgsumbin  22759  chpscmatgsummon  22760  tgplacthmeo  24018  tgpconncomp  24028  qustgpopn  24035  tsmsxplem1  24068  tlmtgp  24111  isngp4  24527  ngpinvds  24528  ngpsubcan  24529  nmtri  24541  ngptgp  24551  tngngp3  24571  ncvspi  25083  deg1suble  26039  deg1sub  26040  dchr2sum  27211  dchrisum0re  27451  symgfcoeu  33051  symgsubg  33056  archirngz  33158  archiabllem1b  33161  archiabllem2c  33164  eqgvscpbl  33315  qusxpid  33328  linds2eq  33346  quslsm  33370  nsgmgclem  33376  ressply1sub  33533  madjusmdetlem3  33842  madjusmdetlem4  33843  lflsub  39176  lflnegcl  39184  ldualvsubcl  39265  ldualvsubval  39266  dvhgrp  41216  lcfrlem2  41652  lcdvsubval  41727  mapdpglem30  41811  baerlem3lem1  41816  baerlem5alem1  41817  baerlem5blem1  41818  baerlem5blem2  41821  fldhmf1  42193  nelsubginvcld  42599  invginvrid  48477  lincext1  48565  lindslinindimp2lem1  48569  ldepsprlem  48583  ldepspr  48584  lincresunit3lem3  48585  lincresunit3lem1  48590  lincresunit3lem2  48591  lincresunit3  48592