Metamath Proof Explorer

Theorem pgpgrp

Description: Reverse closure for the second argument of pGrp . (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Assertion pgpgrp 
|- ( P pGrp G -> G e. Grp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( od ` G ) = ( od ` G )
3 1 2 ispgp 
 |-  ( P pGrp G <-> ( P e. Prime /\ G e. Grp /\ A. x e. ( Base ` G ) E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) )
4 3 simp2bi 
 |-  ( P pGrp G -> G e. Grp )