Theorem pgpgrp

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

	Ref	Expression
Assertion	pgpgrp	⊢ ( 𝑃 pGrp 𝐺 → 𝐺 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2		eqid	⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
3	1 2	ispgp	⊢ ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
4	3	simp2bi	⊢ ( 𝑃 pGrp 𝐺 → 𝐺 ∈ Grp )