Definition df-gex 17949

Description: Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.) (Revised by AV, 26-Sep-2020.)

Assertion

Ref	Expression
df-gex	|- gEx = ( g e. _V |-> [_ { n e. NN | A. x e. ( Base ` g ) ( 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-gex

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

This definition is referenced by:  gexval  17993