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 ( 𝑃 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 )