Definition df-od 16877

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.)

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 , sup ( i , RR , `' < ) ) ) )

Distinct variable group:   g, i, n, x

Detailed syntax breakdown of Definition df-od

Step	Hyp	Ref	Expression
1		cod 16873	. 2 class od
2		vg	. . 3 setvar g
3		cvv 3059	. . 3 class _V
4		vx	. . . 4 setvar x
5	2	cv 1404	. . . . 5 class g
6		cbs 14841	. . . . 5 class Base
7	5, 6	cfv 5569	. . . 4 class ( Base ` g )
8		vi	. . . . 5 setvar i
9		vn	. . . . . . . . 9 setvar n
10	9	cv 1404	. . . . . . . 8 class n
11	4	cv 1404	. . . . . . . 8 class x
12		cmg 16380	. . . . . . . . 9 class .g
13	5, 12	cfv 5569	. . . . . . . 8 class (.g ` g )
14	10, 11, 13	co 6278	. . . . . . 7 class ( n (.g ` g ) x )
15		c0g 15054	. . . . . . . 8 class 0g
16	5, 15	cfv 5569	. . . . . . 7 class ( 0g ` g )
17	14, 16	wceq 1405	. . . . . 6 wff ( n (.g ` g ) x ) = ( 0g ` g )
18		cn 10576	. . . . . 6 class NN
19	17, 9, 18	crab 2758	. . . . 5 class { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) }
20	8	cv 1404	. . . . . . 7 class i
21		c0 3738	. . . . . . 7 class (/)
22	20, 21	wceq 1405	. . . . . 6 wff i = (/)
23		cc0 9522	. . . . . 6 class 0
24		cr 9521	. . . . . . 7 class RR
25		clt 9658	. . . . . . . 8 class <
26	25	ccnv 4822	. . . . . . 7 class `' <
27	20, 24, 26	csup 7934	. . . . . 6 class sup ( i , RR , `' < )
28	22, 23, 27	cif 3885	. . . . 5 class if ( i = (/) , 0 , sup ( i , RR , `' < ) )
29	8, 19, 28	csb 3373	. . . 4 class [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , sup ( i , RR , `' < ) )
30	4, 7, 29	cmpt 4453	. . 3 class ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , sup ( i , RR , `' < ) ) )
31	2, 3, 30	cmpt 4453	. 2 class ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , sup ( i , RR , `' < ) ) ) )
32	1, 31	wceq 1405	1 wff od = ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , sup ( i , RR , `' < ) ) ) )

This definition is referenced by:  odfval  16881