Definition df-pgp 19516

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 19512	. 2 class pGrp
2		vp	. . . . . . 7 setvar 𝑝
3	2	cv 1539	. . . . . 6 class 𝑝
4		cprime 16695	. . . . . 6 class ℙ
5	3, 4	wcel 2109	. . . . 5 wff 𝑝 ∈ ℙ
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1539	. . . . . 6 class 𝑔
8		cgrp 18921	. . . . . 6 class Grp
9	7, 8	wcel 2109	. . . . 5 wff 𝑔 ∈ Grp
10	5, 9	wa 395	. . . 4 wff (𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp)
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1539	. . . . . . . 8 class 𝑥
13		cod 19510	. . . . . . . . 9 class od
14	7, 13	cfv 6536	. . . . . . . 8 class (od‘𝑔)
15	12, 14	cfv 6536	. . . . . . 7 class ((od‘𝑔)‘𝑥)
16		vn	. . . . . . . . 9 setvar 𝑛
17	16	cv 1539	. . . . . . . 8 class 𝑛
18		cexp 14084	. . . . . . . 8 class ↑
19	3, 17, 18	co 7410	. . . . . . 7 class (𝑝↑𝑛)
20	15, 19	wceq 1540	. . . . . 6 wff ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
21		cn0 12506	. . . . . 6 class ℕ0
22	20, 16, 21	wrex 3061	. . . . 5 wff ∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
23		cbs 17233	. . . . . 6 class Base
24	7, 23	cfv 6536	. . . . 5 class (Base‘𝑔)
25	22, 11, 24	wral 3052	. . . 4 wff ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
26	10, 25	wa 395	. . 3 wff ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))
27	26, 2, 6	copab 5186	. 2 class {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))}
28	1, 27	wceq 1540	1 wff pGrp = {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))}

This definition is referenced by:  ispgp  19578