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	|- od = ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )

Distinct variable group:   g, i, n, x

Detailed syntax breakdown of Definition df-od

Step	Hyp	Ref	Expression
1		cod 17177	. 2 class od
2		vg	. . 3 setvar g
3		cvv 3047	. . 3 class _V
4		vx	. . . 4 setvar x
5	2	cv 1445	. . . . 5 class g
6		cbs 15133	. . . . 5 class Base
7	5, 6	cfv 5585	. . . 4 class ( Base ` g )
8		vi	. . . . 5 setvar i
9		vn	. . . . . . . . 9 setvar n
10	9	cv 1445	. . . . . . . 8 class n
11	4	cv 1445	. . . . . . . 8 class x
12		cmg 16684	. . . . . . . . 9 class .g
13	5, 12	cfv 5585	. . . . . . . 8 class (.g ` g )
14	10, 11, 13	co 6295	. . . . . . 7 class ( n (.g ` g ) x )
15		c0g 15350	. . . . . . . 8 class 0g
16	5, 15	cfv 5585	. . . . . . 7 class ( 0g ` g )
17	14, 16	wceq 1446	. . . . . 6 wff ( n (.g ` g ) x ) = ( 0g ` g )
18		cn 10616	. . . . . 6 class NN
19	17, 9, 18	crab 2743	. . . . 5 class { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) }
20	8	cv 1445	. . . . . . 7 class i
21		c0 3733	. . . . . . 7 class (/)
22	20, 21	wceq 1446	. . . . . 6 wff i = (/)
23		cc0 9544	. . . . . 6 class 0
24		cr 9543	. . . . . . 7 class RR
25		clt 9680	. . . . . . 7 class <
26	20, 24, 25	cinf 7960	. . . . . 6 class inf ( i , RR , < )
27	22, 23, 26	cif 3883	. . . . 5 class if ( i = (/) , 0 , inf ( i , RR , < ) )
28	8, 19, 27	csb 3365	. . . 4 class [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) )
29	4, 7, 28	cmpt 4464	. . 3 class ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
30	2, 3, 29	cmpt 4464	. 2 class ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
31	1, 30	wceq 1446	1 wff od = ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )

This definition is referenced by:  odfval  17191