Metamath Proof Explorer

Theorem pgpfi2

Description: Alternate version of pgpfi . (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypothesis pgpfi.1 ⊢ X = Base G
Assertion pgpfi2 ⊢ G ∈ Grp ∧ X ∈ Fin → P pGrp G ↔ P ∈ ℙ ∧ X = P P pCnt X

Proof

Step Hyp Ref Expression
1 pgpfi.1 ⊢ X = Base G
2 1 pgpfi ⊢ G ∈ Grp ∧ X ∈ Fin → P pGrp G ↔ P ∈ ℙ ∧ ∃ n ∈ ℕ 0 X = P n
3 id ⊢ P ∈ ℙ → P ∈ ℙ
4 1 grpbn0 ⊢ G ∈ Grp → X ≠ ∅
5 hashnncl ⊢ X ∈ Fin → X ∈ ℕ ↔ X ≠ ∅
6 4 5 syl5ibrcom ⊢ G ∈ Grp → X ∈ Fin → X ∈ ℕ
7 6 imp ⊢ G ∈ Grp ∧ X ∈ Fin → X ∈ ℕ
8 pcprmpw ⊢ P ∈ ℙ ∧ X ∈ ℕ → ∃ n ∈ ℕ 0 X = P n ↔ X = P P pCnt X
9 3 7 8 syl2anr ⊢ G ∈ Grp ∧ X ∈ Fin ∧ P ∈ ℙ → ∃ n ∈ ℕ 0 X = P n ↔ X = P P pCnt X
10 9 pm5.32da ⊢ G ∈ Grp ∧ X ∈ Fin → P ∈ ℙ ∧ ∃ n ∈ ℕ 0 X = P n ↔ P ∈ ℙ ∧ X = P P pCnt X
11 2 10 bitrd ⊢ G ∈ Grp ∧ X ∈ Fin → P pGrp G ↔ P ∈ ℙ ∧ X = P P pCnt X