Definition df-pgp 17950

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.)

Assertion

Ref	Expression
df-pgp	|- pGrp = { <. p , g >. | ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) ) }

Distinct variable group:   g, n, p, x

Detailed syntax breakdown of Definition df-pgp

Step	Hyp	Ref	Expression
1		cpgp 17946	. 2 class pGrp
2		vp	. . . . . . 7 setvar p
3	2	cv 1482	. . . . . 6 class p
4		cprime 15385	. . . . . 6 class Prime
5	3, 4	wcel 1990	. . . . 5 wff p e. Prime
6		vg	. . . . . . 7 setvar g
7	6	cv 1482	. . . . . 6 class g
8		cgrp 17422	. . . . . 6 class Grp
9	7, 8	wcel 1990	. . . . 5 wff g e. Grp
10	5, 9	wa 384	. . . 4 wff ( p e. Prime /\ g e. Grp )
11		vx	. . . . . . . . 9 setvar x
12	11	cv 1482	. . . . . . . 8 class x
13		cod 17944	. . . . . . . . 9 class od
14	7, 13	cfv 5888	. . . . . . . 8 class ( od ` g )
15	12, 14	cfv 5888	. . . . . . 7 class ( ( od ` g ) ` x )
16		vn	. . . . . . . . 9 setvar n
17	16	cv 1482	. . . . . . . 8 class n
18		cexp 12860	. . . . . . . 8 class ^
19	3, 17, 18	co 6650	. . . . . . 7 class ( p ^ n )
20	15, 19	wceq 1483	. . . . . 6 wff ( ( od ` g ) ` x ) = ( p ^ n )
21		cn0 11292	. . . . . 6 class NN0
22	20, 16, 21	wrex 2913	. . . . 5 wff E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n )
23		cbs 15857	. . . . . 6 class Base
24	7, 23	cfv 5888	. . . . 5 class ( Base ` g )
25	22, 11, 24	wral 2912	. . . 4 wff A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n )
26	10, 25	wa 384	. . 3 wff ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) )
27	26, 2, 6	copab 4712	. 2 class { <. p , g >. | ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) ) }
28	1, 27	wceq 1483	1 wff pGrp = { <. p , g >. | ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) ) }

This definition is referenced by:  ispgp  18007