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

Definition df-gex 17123
 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.)
Assertion
Ref Expression
df-gex gEx .g inf
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-gex
StepHypRef Expression
1 cgex 17118 . 2 gEx
2 vg . . 3
3 cvv 3078 . . 3
4 vi . . . 4
5 vn . . . . . . . . 9
65cv 1436 . . . . . . . 8
7 vx . . . . . . . . 9
87cv 1436 . . . . . . . 8
92cv 1436 . . . . . . . . 9
10 cmg 16624 . . . . . . . . 9 .g
119, 10cfv 5592 . . . . . . . 8 .g
126, 8, 11co 6296 . . . . . . 7 .g
13 c0g 15298 . . . . . . . 8
149, 13cfv 5592 . . . . . . 7
1512, 14wceq 1437 . . . . . 6 .g
16 cbs 15081 . . . . . . 7
179, 16cfv 5592 . . . . . 6
1815, 7, 17wral 2773 . . . . 5 .g
19 cn 10598 . . . . 5
2018, 5, 19crab 2777 . . . 4 .g
214cv 1436 . . . . . 6
22 c0 3758 . . . . . 6
2321, 22wceq 1437 . . . . 5
24 cc0 9528 . . . . 5
25 cr 9527 . . . . . 6
26 clt 9664 . . . . . 6
2721, 25, 26cinf 7952 . . . . 5 inf
2823, 24, 27cif 3906 . . . 4 inf
294, 20, 28csb 3392 . . 3 .g inf
302, 3, 29cmpt 4475 . 2 .g inf
311, 30wceq 1437 1 gEx .g inf
 Colors of variables: wff setvar class This definition is referenced by:  gexval  17168
 Copyright terms: Public domain W3C validator