Definition 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 = { ⟨ 𝑝 , 𝑔 ⟩ ∣ ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpgp	⊢ pGrp
1		vp	⊢ 𝑝
2		vg	⊢ 𝑔
3	1	cv	⊢ 𝑝
4		cprime	⊢ ℙ
5	3 4	wcel	⊢ 𝑝 ∈ ℙ
6	2	cv	⊢ 𝑔
7		cgrp	⊢ Grp
8	6 7	wcel	⊢ 𝑔 ∈ Grp
9	5 8	wa	⊢ ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp )
10		vx	⊢ 𝑥
11		cbs	⊢ Base
12	6 11	cfv	⊢ ( Base ‘ 𝑔 )
13		vn	⊢ 𝑛
14		cn0	⊢ ℕ0
15		cod	⊢ od
16	6 15	cfv	⊢ ( od ‘ 𝑔 )
17	10	cv	⊢ 𝑥
18	17 16	cfv	⊢ ( ( od ‘ 𝑔 ) ‘ 𝑥 )
19		cexp	⊢ ↑
20	13	cv	⊢ 𝑛
21	3 20 19	co	⊢ ( 𝑝 ↑ 𝑛 )
22	18 21	wceq	⊢ ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 )
23	22 13 14	wrex	⊢ ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 )
24	23 10 12	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 )
25	9 24	wa	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) )
26	25 1 2	copab	⊢ { ⟨ 𝑝 , 𝑔 ⟩ ∣ ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) ) }
27	0 26	wceq	⊢ pGrp = { ⟨ 𝑝 , 𝑔 ⟩ ∣ ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) ) }