Theorem grpoinvcl

Description: A group element's inverse is a group element. (Contributed by NM, 27-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpinvcl.1	|- X = ran G
	grpinvcl.2	|- N = ( inv ` G )
Assertion	grpoinvcl	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) e. X )

Proof

Step	Hyp	Ref	Expression
1		grpinvcl.1	|- X = ran G
2		grpinvcl.2	|- N = ( inv ` G )
3		eqid	|- ( GId ` G ) = ( GId ` G )
4	1 3 2	grpoinvval	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) = ( iota_ y e. X ( y G A ) = ( GId ` G ) ) )
5	1 3	grpoinveu	|- ( ( G e. GrpOp /\ A e. X ) -> E! y e. X ( y G A ) = ( GId ` G ) )
6		riotacl	|- ( E! y e. X ( y G A ) = ( GId ` G ) -> ( iota_ y e. X ( y G A ) = ( GId ` G ) ) e. X )
7	5 6	syl	|- ( ( G e. GrpOp /\ A e. X ) -> ( iota_ y e. X ( y G A ) = ( GId ` G ) ) e. X )
8	4 7	eqeltrd	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) e. X )