Description: Reverse closure for the second argument of pGrp . (Contributed by Mario Carneiro, 15-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | pgpgrp | ⊢ ( 𝑃 pGrp 𝐺 → 𝐺 ∈ Grp ) |
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 ) |