Theorem grpinvcl 19213

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ‘cfv 6547  Basecbs 17402  Grpcgrp 19159  inv_gcminusg 19160

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-fv 6555  df-riota 7387  df-ov 7433  df-0g 17627  df-mgm 18831  df-sgrp 18923  df-mnd 18939  df-grp 19162  df-minusg 19163

This theorem is used by:  grpinvcld  19214  grprinv  19216  grpinvid1  19217  grpinvid2  19218  grplrinv  19222  grplcan  19226  grpasscan1  19227  grpasscan2  19228  grpinvinv  19231  grpinvcnv  19232  grpinvnzcl  19236  grpsubinv  19237  grplmulf1o  19238  grpinvssd  19242  grpinvadd  19243  grpsubf  19244  grpsubrcan  19246  grpinvsub  19247  grpinvval2  19248  grpsubeq0  19251  grpsubadd  19253  grpaddsubass  19255  grpnpcan  19257  dfgrp3  19264  grplactcnv  19268  grpsubpropd2  19271  prdsinvlem  19274  pwssub  19279  imasgrp  19281  ghmgrp  19291  mulgcl  19316  mulgaddcomlem  19322  mulginvcom  19324  mulginvinv  19325  mulgneg2  19333  subginv  19358  subginvcl  19360  issubg4  19371  grpissubg  19372  isnsg3  19385  subgacs  19386  nmzsubg  19390  eqglact  19406  eqgcpbl  19409  qusxpid  19410  qusgrp  19416  qusinv  19420  qussub  19421  eqg0subg  19426  ghminv  19452  ghmsub  19453  ghmrn  19458  ghmpreima  19467  ghmeql  19468  conjghm  19478  galcan  19533  gacan  19534  gapm  19535  gaorber  19537  gastacl  19538  gastacos  19539  cntzsubg  19568  oppggrp  19586  symgsssg  19696  symgfisg  19697  odinv  19790  sylow2blem1  19849  sylow2blem3  19851  frgpuptf  19999  frgpuplem  20001  ablinvadd  20036  ablsub2inv  20037  ablsub4  20039  ablsubsub4  20047  mulgsubdi  20058  invghm  20062  eqgabl  20063  torsubg  20083  oddvdssubg  20084  cyggeninv  20112  ogrpinv0le  20365  ogrpsub  20366  ogrpaddltbi  20368  ogrpaddltrbid  20370  ogrpinv0lt  20372  ogrpinvlt  20373  ringnegl  20548  ringnegr  20549  ringmneg1  20550  ringmneg2  20551  dvdsrneg  20615  unitinvcl  20635  unitnegcl  20642  cntzsubr  20873  isdrng2  21012  isdrng3lem1  21020  abvneg  21098  abvsubtri  21099  orngsqr  21138  lmodvnegcl  21193  lmodvneg1  21195  lmodvsneg  21196  lmodsubvs  21208  lmodsubdi  21209  lmodsubdir  21210  lssvsubcl  21234  lspsnneg  21296  lmodvsinv  21326  lmodvsinv2  21327  lspexch  21422  lspsolvlem  21435  zrhpsgninv  21906  evpmodpmf1o  21917  dsmmsubg  22064  mplsubglem  22321  mplind  22394  cpmatinvcl  23050  chpscmatgsumbin  23177  chpscmatgsummon  23178  tgplacthmeo  24437  tgpconncomp  24447  qustgpopn  24454  tsmsxplem1  24487  tlmtgp  24530  isngp4  24946  ngpinvds  24947  ngpsubcan  24948  nmtri  24960  ngptgp  24970  tngngp3  24990  ncvspi  25492  deg1suble  26440  deg1sub  26441  dchr2sum  27615  dchrisum0re  27855  symgfcoeu  33699  symgsubg  33704  archirngz  33806  archiabllem1b  33809  archiabllem2c  33812  eqgvscpbl  33967  linds2eq  33992  quslsm  34012  nsgmgclem  34018  ressply1sub  34158  madjusmdetlem3  34517  madjusmdetlem4  34518  lflsub  40267  lflnegcl  40275  ldualvsubcl  40356  ldualvsubval  40357  dvhgrp  42307  lcfrlem2  42743  lcdvsubval  42818  mapdpglem30  42902  baerlem3lem1  42907  baerlem5alem1  42908  baerlem5blem1  42909  baerlem5blem2  42912  fldhmf1  43283  nelsubginvcld  43703  invginvrid  49621  lincext1  49708  lindslinindimp2lem1  49712  ldepsprlem  49726  ldepspr  49727  lincresunit3lem3  49728  lincresunit3lem1  49733  lincresunit3lem2  49734  lincresunit3  49735