This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odcl2

Description: The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses odcl2.1 
|- X = ( Base ` G )
odcl2.2 
|- O = ( od ` G )
Assertion odcl2 
|- ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( O ` A ) e. NN )

Proof

Step Hyp Ref Expression
1 odcl2.1 
 |-  X = ( Base ` G )
2 odcl2.2 
 |-  O = ( od ` G )
3 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
4 3 adantl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) e. NN0 )
5 elnn0 
 |-  ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
6 4 5 sylib 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
7 6 ord 
 |-  ( ( G e. Grp /\ A e. X ) -> ( -. ( O ` A ) e. NN -> ( O ` A ) = 0 ) )
8 eqid 
 |-  ( .g ` G ) = ( .g ` G )
9 eqid 
 |-  ( x e. ZZ |-> ( x ( .g ` G ) A ) ) = ( x e. ZZ |-> ( x ( .g ` G ) A ) )
10 1 2 8 9 odinf 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. Fin )
11 1 2 8 9 odf1 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 <-> ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ -1-1-> X ) )
12 11 biimp3a 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ -1-1-> X )
13 f1f 
 |-  ( ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ -1-1-> X -> ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ --> X )
14 frn 
 |-  ( ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ --> X -> ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) C_ X )
15 ssfi 
 |-  ( ( X e. Fin /\ ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) C_ X ) -> ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. Fin )
16 15 expcom 
 |-  ( ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) C_ X -> ( X e. Fin -> ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. Fin ) )
17 12 13 14 16 4syl 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( X e. Fin -> ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. Fin ) )
18 10 17 mtod 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. X e. Fin )
19 18 3expia 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 -> -. X e. Fin ) )
20 7 19 syld 
 |-  ( ( G e. Grp /\ A e. X ) -> ( -. ( O ` A ) e. NN -> -. X e. Fin ) )
21 20 con4d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( X e. Fin -> ( O ` A ) e. NN ) )
22 21 3impia 
 |-  ( ( G e. Grp /\ A e. X /\ X e. Fin ) -> ( O ` A ) e. NN )
23 22 3com23 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( O ` A ) e. NN )