Theorem pgpgrp

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

	Ref	Expression
Assertion	pgpgrp	$$⊢P\mathrm{pGrp}G\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
2		eqid	$$⊢\mathrm{od}\left(G\right)=\mathrm{od}\left(G\right)$$
3	1 2	ispgp	$$⊢P\mathrm{pGrp}G\leftrightarrow \left(P\in \mathbb{P}\wedge G\in \mathrm{Grp}\wedge \forall x\in {\mathrm{Base}}_G\exists n\in {\mathbb{N}}_0\mathrm{od}\left(G\right)\left(x\right)=P^n\right)$$
4	3	simp2bi	$$⊢P\mathrm{pGrp}G\to G\in \mathrm{Grp}$$