Definition df-pgp 17773

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

Assertion

Ref	Expression
df-pgp	⊢ pGrp = {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))}

Distinct variable group:   𝑔,𝑛,𝑝,𝑥

Detailed syntax breakdown of Definition df-pgp

Step	Hyp	Ref	Expression
1		cpgp 17769	. 2 class pGrp
2		vp	. . . . . . 7 setvar 𝑝
3	2	cv 1474	. . . . . 6 class 𝑝
4		cprime 15223	. . . . . 6 class ℙ
5	3, 4	wcel 1977	. . . . 5 wff 𝑝 ∈ ℙ
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1474	. . . . . 6 class 𝑔
8		cgrp 17245	. . . . . 6 class Grp
9	7, 8	wcel 1977	. . . . 5 wff 𝑔 ∈ Grp
10	5, 9	wa 383	. . . 4 wff (𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp)
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1474	. . . . . . . 8 class 𝑥
13		cod 17767	. . . . . . . . 9 class od
14	7, 13	cfv 5804	. . . . . . . 8 class (od‘𝑔)
15	12, 14	cfv 5804	. . . . . . 7 class ((od‘𝑔)‘𝑥)
16		vn	. . . . . . . . 9 setvar 𝑛
17	16	cv 1474	. . . . . . . 8 class 𝑛
18		cexp 12722	. . . . . . . 8 class ↑
19	3, 17, 18	co 6549	. . . . . . 7 class (𝑝↑𝑛)
20	15, 19	wceq 1475	. . . . . 6 wff ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
21		cn0 11169	. . . . . 6 class ℕ0
22	20, 16, 21	wrex 2897	. . . . 5 wff ∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
23		cbs 15695	. . . . . 6 class Base
24	7, 23	cfv 5804	. . . . 5 class (Base‘𝑔)
25	22, 11, 24	wral 2896	. . . 4 wff ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
26	10, 25	wa 383	. . 3 wff ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))
27	26, 2, 6	copab 4642	. 2 class {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))}
28	1, 27	wceq 1475	1 wff pGrp = {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))}

This definition is referenced by:  ispgp  17830