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