Metamath Proof Explorer


Theorem grpinvcld

Description: A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025)

Ref Expression
Hypotheses grpinvcld.b
|- B = ( Base ` G )
grpinvcld.n
|- N = ( invg ` G )
grpinvcld.g
|- ( ph -> G e. Grp )
grpinvcld.1
|- ( ph -> X e. B )
Assertion grpinvcld
|- ( ph -> ( N ` X ) e. B )

Proof

Step Hyp Ref Expression
1 grpinvcld.b
 |-  B = ( Base ` G )
2 grpinvcld.n
 |-  N = ( invg ` G )
3 grpinvcld.g
 |-  ( ph -> G e. Grp )
4 grpinvcld.1
 |-  ( ph -> X e. B )
5 1 2 grpinvcl
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
6 3 4 5 syl2anc
 |-  ( ph -> ( N ` X ) e. B )