Metamath Proof Explorer

Definition df-pgp

Description: Define the set of p-groups, which are groups such that every element has a power of p as its order. (Contributed by Mario Carneiro, 15-Jan-2015) (Revised by AV, 5-Oct-2020)

Ref Expression
Assertion df-pgp ⊢ pGrp = p g | p ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpgp class pGrp
1 vp setvar p
2 vg setvar g
3 1 cv setvar p
4 cprime class ℙ
5 3 4 wcel wff p ∈ ℙ
6 2 cv setvar g
7 cgrp class Grp
8 6 7 wcel wff g ∈ Grp
9 5 8 wa wff p ∈ ℙ ∧ g ∈ Grp
10 vx setvar x
11 cbs class Base
12 6 11 cfv class Base g
13 vn setvar n
14 cn0 class ℕ 0
15 cod class od
16 6 15 cfv class od ⁡ g
17 10 cv setvar x
18 17 16 cfv class od ⁡ g ⁡ x
19 cexp class ^
20 13 cv setvar n
21 3 20 19 co class p n
22 18 21 wceq wff od ⁡ g ⁡ x = p n
23 22 13 14 wrex wff ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n
24 23 10 12 wral wff ∀ x ∈ Base g ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n
25 9 24 wa wff p ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n
26 25 1 2 copab class p g | p ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n
27 0 26 wceq wff pGrp = p g | p ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n