Metamath Proof Explorer


Definition df-gex

Description: Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by Stefan O'Rear, 4-Sep-2015) (Revised by AV, 26-Sep-2020)

Ref Expression
Assertion df-gex gEx=gVn|xBasegngx=0g/iifi=0supi<

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgex classgEx
1 vg setvarg
2 cvv classV
3 vn setvarn
4 cn class
5 vx setvarx
6 cbs classBase
7 1 cv setvarg
8 7 6 cfv classBaseg
9 3 cv setvarn
10 cmg class𝑔
11 7 10 cfv classg
12 5 cv setvarx
13 9 12 11 co classngx
14 c0g class0𝑔
15 7 14 cfv class0g
16 13 15 wceq wffngx=0g
17 16 5 8 wral wffxBasegngx=0g
18 17 3 4 crab classn|xBasegngx=0g
19 vi setvari
20 19 cv setvari
21 c0 class
22 20 21 wceq wffi=
23 cc0 class0
24 cr class
25 clt class<
26 20 24 25 cinf classsupi<
27 22 23 26 cif classifi=0supi<
28 19 18 27 csb classn|xBasegngx=0g/iifi=0supi<
29 1 2 28 cmpt classgVn|xBasegngx=0g/iifi=0supi<
30 0 29 wceq wffgEx=gVn|xBasegngx=0g/iifi=0supi<