Definition df-pgp 19053

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 19049	. 2 class pGrp
2		vp	. . . . . . 7 setvar 𝑝
3	2	cv 1538	. . . . . 6 class 𝑝
4		cprime 16304	. . . . . 6 class ℙ
5	3, 4	wcel 2108	. . . . 5 wff 𝑝 ∈ ℙ
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1538	. . . . . 6 class 𝑔
8		cgrp 18492	. . . . . 6 class Grp
9	7, 8	wcel 2108	. . . . 5 wff 𝑔 ∈ Grp
10	5, 9	wa 395	. . . 4 wff (𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp)
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1538	. . . . . . . 8 class 𝑥
13		cod 19047	. . . . . . . . 9 class od
14	7, 13	cfv 6418	. . . . . . . 8 class (od‘𝑔)
15	12, 14	cfv 6418	. . . . . . 7 class ((od‘𝑔)‘𝑥)
16		vn	. . . . . . . . 9 setvar 𝑛
17	16	cv 1538	. . . . . . . 8 class 𝑛
18		cexp 13710	. . . . . . . 8 class ↑
19	3, 17, 18	co 7255	. . . . . . 7 class (𝑝↑𝑛)
20	15, 19	wceq 1539	. . . . . 6 wff ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
21		cn0 12163	. . . . . 6 class ℕ0
22	20, 16, 21	wrex 3064	. . . . 5 wff ∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
23		cbs 16840	. . . . . 6 class Base
24	7, 23	cfv 6418	. . . . 5 class (Base‘𝑔)
25	22, 11, 24	wral 3063	. . . 4 wff ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛)
26	10, 25	wa 395	. . 3 wff ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))
27	26, 2, 6	copab 5132	. 2 class {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))}
28	1, 27	wceq 1539	1 wff pGrp = {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))}

This definition is referenced by:  ispgp  19112