Definition df-od 15122

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 15118	. 2 class od
2		vg	. . 3 set g
3		cvv 2916	. . 3 class _V
4		vx	. . . 4 set x
5	2	cv 1648	. . . . 5 class g
6		cbs 13424	. . . . 5 class Base
7	5, 6	cfv 5413	. . . 4 class ( Base ` g )
8		vi	. . . . 5 set i
9		vn	. . . . . . . . 9 set n
10	9	cv 1648	. . . . . . . 8 class n
11	4	cv 1648	. . . . . . . 8 class x
12		cmg 14644	. . . . . . . . 9 class .g
13	5, 12	cfv 5413	. . . . . . . 8 class (.g ` g )
14	10, 11, 13	co 6040	. . . . . . 7 class ( n (.g ` g ) x )
15		c0g 13678	. . . . . . . 8 class 0g
16	5, 15	cfv 5413	. . . . . . 7 class ( 0g ` g )
17	14, 16	wceq 1649	. . . . . 6 wff ( n (.g ` g ) x ) = ( 0g ` g )
18		cn 9956	. . . . . 6 class NN
19	17, 9, 18	crab 2670	. . . . 5 class { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) }
20	8	cv 1648	. . . . . . 7 class i
21		c0 3588	. . . . . . 7 class (/)
22	20, 21	wceq 1649	. . . . . 6 wff i = (/)
23		cc0 8946	. . . . . 6 class 0
24		cr 8945	. . . . . . 7 class RR
25		clt 9076	. . . . . . . 8 class <
26	25	ccnv 4836	. . . . . . 7 class `' <
27	20, 24, 26	csup 7403	. . . . . 6 class sup ( i , RR , `' < )
28	22, 23, 27	cif 3699	. . . . 5 class if ( i = (/) , 0 , sup ( i , RR , `' < ) )
29	8, 19, 28	csb 3211	. . . 4 class [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , sup ( i , RR , `' < ) )
30	4, 7, 29	cmpt 4226	. . 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 4226	. 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 1649	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  15126