This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )