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 \in ℙ \land g \in Grp) \land \forall x \in {Base}_{g} \exists n \in ℕ_{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 \in ℙ$
6	2	cv	$setvar g$
7		cgrp	$class Grp$
8	6 7	wcel	$wff g \in Grp$
9	5 8	wa	$wff (p \in ℙ \land g \in 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 \exists n \in ℕ_{0} od (g) (x) = p^{n}$
24	23 10 12	wral	$wff \forall x \in {Base}_{g} \exists n \in ℕ_{0} od (g) (x) = p^{n}$
25	9 24	wa	$wff ((p \in ℙ \land g \in Grp) \land \forall x \in {Base}_{g} \exists n \in ℕ_{0} od (g) (x) = p^{n})$
26	25 1 2	copab	$class \{⟨p, g⟩ \| ((p \in ℙ \land g \in Grp) \land \forall x \in {Base}_{g} \exists n \in ℕ_{0} od (g) (x) = p^{n})\}$
27	0 26	wceq	$wff pGrp = \{⟨p, g⟩ \| ((p \in ℙ \land g \in Grp) \land \forall x \in {Base}_{g} \exists n \in ℕ_{0} od (g) (x) = p^{n})\}$

Metamath Proof Explorer

Definition df-pgp

Detailed syntax breakdown