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 = inv g G
grpinvcld.g φ G Grp
grpinvcld.1 φ X B
Assertion grpinvcld φ N X B

Proof

Step Hyp Ref Expression
1 grpinvcld.b B = Base G
2 grpinvcld.n N = inv g G
3 grpinvcld.g φ G Grp
4 grpinvcld.1 φ X B
5 1 2 grpinvcl G Grp X B N X B
6 3 4 5 syl2anc φ N X B