Theorem grpinvcl 13094

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2160  ‘cfv 5242  Basecbs 12592  Grpcgrp 13046  inv_gcminusg 13047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4140  ax-sep 4143  ax-pow 4199  ax-pr 4234  ax-un 4458  ax-cnex 7949  ax-resscn 7950  ax-1re 7952  ax-addrcl 7955

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2758  df-sbc 2982  df-csb 3077  df-un 3153  df-in 3155  df-ss 3162  df-pw 3599  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-int 3867  df-iun 3910  df-br 4026  df-opab 4087  df-mpt 4088  df-id 4318  df-xp 4657  df-rel 4658  df-cnv 4659  df-co 4660  df-dm 4661  df-rn 4662  df-res 4663  df-ima 4664  df-iota 5203  df-fun 5244  df-fn 5245  df-f 5246  df-f1 5247  df-fo 5248  df-f1o 5249  df-fv 5250  df-riota 5861  df-ov 5909  df-inn 8969  df-2 9027  df-ndx 12595  df-slot 12596  df-base 12598  df-plusg 12682  df-0g 12843  df-mgm 12913  df-sgrp 12959  df-mnd 12972  df-grp 13049  df-minusg 13050

This theorem is referenced by:  grpinvcld  13095  grprinv  13097  grpinvid1  13098  grpinvid2  13099  grplrinv  13103  grpressid  13107  grplcan  13108  grpasscan1  13109  grpasscan2  13110  grpinvinv  13113  grpinvcnv  13114  grpinvnzcl  13118  grpsubinv  13119  grplmulf1o  13120  grpinvssd  13123  grpinvadd  13124  grpsubf  13125  grpsubrcan  13127  grpinvsub  13128  grpinvval2  13129  grpsubeq0  13132  grpsubadd  13134  grpaddsubass  13136  grpnpcan  13138  dfgrp3m  13145  grplactcnv  13148  grpsubpropd2  13151  imasgrp  13155  ghmgrp  13162  mulgcl  13183  mulgaddcomlem  13189  mulginvcom  13191  mulginvinv  13192  mulgneg2  13200  subginv  13224  subginvcl  13226  issubg4m  13236  grpissubg  13237  subgintm  13241  0subg  13242  isnsg3  13250  nmzsubg  13253  eqger  13267  eqglact  13268  eqgcpbl  13271  qusgrp  13275  qusinv  13279  qussub  13280  ghminv  13293  ghmsub  13294  ghmrn  13300  ghmpreima  13309  ghmeql  13310  conjghm  13319  ablinvadd  13353  ablsub2inv  13354  ablsub4  13356  ablsubsub4  13362  invghm  13372  eqgabl  13373  ringnegl  13511  ringnegr  13512  ringmneg1  13513  ringmneg2  13514  ringm2neg  13515  ringsubdi  13516  ringsubdir  13517  dvdsrneg  13563  unitinvcl  13583  unitnegcl  13590  lmodvnegcl  13788  lmodvneg1  13790  lmodvsneg  13791  lmodsubvs  13803  lmodsubdi  13804  lmodsubdir  13805  lssvsubcl  13826  lssvnegcl  13836  lspsnneg  13880