Metamath Proof Explorer


Theorem gexcl

Description: The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016)

Ref Expression
Hypotheses gexcl.1
|- X = ( Base ` G )
gexcl.2
|- E = ( gEx ` G )
Assertion gexcl
|- ( G e. V -> E e. NN0 )

Proof

Step Hyp Ref Expression
1 gexcl.1
 |-  X = ( Base ` G )
2 gexcl.2
 |-  E = ( gEx ` G )
3 eqid
 |-  ( .g ` G ) = ( .g ` G )
4 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
5 eqid
 |-  { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } = { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) }
6 1 3 4 2 5 gexlem1
 |-  ( G e. V -> ( ( E = 0 /\ { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } = (/) ) \/ E e. { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } ) )
7 simpl
 |-  ( ( E = 0 /\ { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } = (/) ) -> E = 0 )
8 elrabi
 |-  ( E e. { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } -> E e. NN )
9 7 8 orim12i
 |-  ( ( ( E = 0 /\ { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } = (/) ) \/ E e. { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } ) -> ( E = 0 \/ E e. NN ) )
10 6 9 syl
 |-  ( G e. V -> ( E = 0 \/ E e. NN ) )
11 10 orcomd
 |-  ( G e. V -> ( E e. NN \/ E = 0 ) )
12 elnn0
 |-  ( E e. NN0 <-> ( E e. NN \/ E = 0 ) )
13 11 12 sylibr
 |-  ( G e. V -> E e. NN0 )