Theorem grpinvcl 13853

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  ‘cfv 5377  Basecbs 13352  Grpcgrp 13805  inv_gcminusg 13806

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-riota 6038  df-ov 6088  df-inn 9305  df-2 9363  df-ndx 13355  df-slot 13356  df-base 13358  df-plusg 13444  df-0g 13612  df-mgm 13676  df-sgrp 13717  df-mnd 13730  df-grp 13808  df-minusg 13809

This theorem is used by:  grpinvcld  13854  grprinv  13856  grpinvid1  13857  grpinvid2  13858  grplrinv  13862  grpressid  13866  grplcan  13867  grpasscan1  13868  grpasscan2  13869  grpinvinv  13872  grpinvcnv  13873  grpinvnzcl  13877  grpsubinv  13878  grplmulf1o  13879  grpinvssd  13882  grpinvadd  13883  grpsubf  13884  grpsubrcan  13886  grpinvsub  13887  grpinvval2  13888  grpsubeq0  13891  grpsubadd  13893  grpaddsubass  13895  grpnpcan  13897  dfgrp3m  13904  grplactcnv  13907  grpsubpropd2  13910  imasgrp  13914  ghmgrp  13921  mulgcl  13942  mulgaddcomlem  13948  mulginvcom  13950  mulginvinv  13951  mulgneg2  13959  subginv  13984  subginvcl  13986  issubg4m  13996  grpissubg  13997  subgintm  14001  0subg  14002  isnsg3  14010  nmzsubg  14013  eqger  14027  eqglact  14028  eqgcpbl  14031  qusgrp  14035  qusinv  14039  qussub  14040  ghminv  14053  ghmsub  14054  ghmrn  14060  ghmpreima  14069  ghmeql  14070  conjghm  14079  ablinvadd  14114  ablsub2inv  14115  ablsub4  14117  ablsubsub4  14123  invghm  14133  eqgabl  14134  pwssub  14216  ringnegl  14356  ringnegr  14357  ringmneg1  14358  ringmneg2  14359  ringm2neg  14360  ringsubdi  14361  ringsubdir  14362  dvdsrneg  14410  unitinvcl  14430  unitnegcl  14437  lmodvnegcl  14665  lmodvneg1  14667  lmodvsneg  14668  lmodsubvs  14680  lmodsubdi  14681  lmodsubdir  14682  lssvsubcl  14703  lssvnegcl  14713  lspsnneg  14757  psrlinv  15075