Theorem grpinvcl

Description: A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 4-May-2015)

	Ref	Expression
Hypotheses	grpinvcl.b	$$⊢B={\mathrm{Base}}_G$$
	grpinvcl.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		grpinvcl.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinvcl.n	$$⊢N={inv}_g\left(G\right)$$
3	1 2	grpinvf	$$⊢G\in \mathrm{Grp}\to N:B⟶B$$
4	3	ffvelcdmda	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in B$$