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