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

Definition df-od 17184
 Description: Define the order of an element in a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.) (Revised by AV, 5-Oct-2020.)
Assertion
Ref Expression
df-od .g inf
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-od
StepHypRef Expression
1 cod 17177 . 2
2 vg . . 3
3 cvv 3047 . . 3
4 vx . . . 4
52cv 1445 . . . . 5
6 cbs 15133 . . . . 5
75, 6cfv 5585 . . . 4
8 vi . . . . 5
9 vn . . . . . . . . 9
109cv 1445 . . . . . . . 8
114cv 1445 . . . . . . . 8
12 cmg 16684 . . . . . . . . 9 .g
135, 12cfv 5585 . . . . . . . 8 .g
1410, 11, 13co 6295 . . . . . . 7 .g
15 c0g 15350 . . . . . . . 8
165, 15cfv 5585 . . . . . . 7
1714, 16wceq 1446 . . . . . 6 .g
18 cn 10616 . . . . . 6
1917, 9, 18crab 2743 . . . . 5 .g
208cv 1445 . . . . . . 7
21 c0 3733 . . . . . . 7
2220, 21wceq 1446 . . . . . 6
23 cc0 9544 . . . . . 6
24 cr 9543 . . . . . . 7
25 clt 9680 . . . . . . 7
2620, 24, 25cinf 7960 . . . . . 6 inf
2722, 23, 26cif 3883 . . . . 5 inf
288, 19, 27csb 3365 . . . 4 .g inf
294, 7, 28cmpt 4464 . . 3 .g inf
302, 3, 29cmpt 4464 . 2 .g inf
311, 30wceq 1446 1 .g inf
 Colors of variables: wff setvar class This definition is referenced by:  odfval  17191
 Copyright terms: Public domain W3C validator