MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pgp Unicode version

Definition df-pgp 16122
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.)
Assertion
Ref Expression
df-pgp
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-pgp
StepHypRef Expression
1 cpgp 16118 . 2
2 vp . . . . . . 7
32cv 1369 . . . . . 6
4 cprime 13849 . . . . . 6
53, 4wcel 1757 . . . . 5
6 vg . . . . . . 7
76cv 1369 . . . . . 6
8 cgrp 15496 . . . . . 6
97, 8wcel 1757 . . . . 5
105, 9wa 369 . . . 4
11 vx . . . . . . . . 9
1211cv 1369 . . . . . . . 8
13 cod 16116 . . . . . . . . 9
147, 13cfv 5500 . . . . . . . 8
1512, 14cfv 5500 . . . . . . 7
16 vn . . . . . . . . 9
1716cv 1369 . . . . . . . 8
18 cexp 11950 . . . . . . . 8
193, 17, 18co 6174 . . . . . . 7
2015, 19wceq 1370 . . . . . 6
21 cn0 10664 . . . . . 6
2220, 16, 21wrex 2793 . . . . 5
23 cbs 14260 . . . . . 6
247, 23cfv 5500 . . . . 5
2522, 11, 24wral 2792 . . . 4
2610, 25wa 369 . . 3
2726, 2, 6copab 4431 . 2
281, 27wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  ispgp  16179
  Copyright terms: Public domain W3C validator