Definition df-od 17948

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 17944	. 2 class od
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5	2	cv 1482	. . . . 5 class g
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` g )
8		vi	. . . . 5 setvar i
9		vn	. . . . . . . . 9 setvar n
10	9	cv 1482	. . . . . . . 8 class n
11	4	cv 1482	. . . . . . . 8 class x
12		cmg 17540	. . . . . . . . 9 class .g
13	5, 12	cfv 5888	. . . . . . . 8 class (.g ` g )
14	10, 11, 13	co 6650	. . . . . . 7 class ( n (.g ` g ) x )
15		c0g 16100	. . . . . . . 8 class 0g
16	5, 15	cfv 5888	. . . . . . 7 class ( 0g ` g )
17	14, 16	wceq 1483	. . . . . 6 wff ( n (.g ` g ) x ) = ( 0g ` g )
18		cn 11020	. . . . . 6 class NN
19	17, 9, 18	crab 2916	. . . . 5 class { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) }
20	8	cv 1482	. . . . . . 7 class i
21		c0 3915	. . . . . . 7 class (/)
22	20, 21	wceq 1483	. . . . . 6 wff i = (/)
23		cc0 9936	. . . . . 6 class 0
24		cr 9935	. . . . . . 7 class RR
25		clt 10074	. . . . . . 7 class <
26	20, 24, 25	cinf 8347	. . . . . 6 class inf ( i , RR , < )
27	22, 23, 26	cif 4086	. . . . 5 class if ( i = (/) , 0 , inf ( i , RR , < ) )
28	8, 19, 27	csb 3533	. . . 4 class [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) )
29	4, 7, 28	cmpt 4729	. . 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 4729	. 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 1483	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  17952