Step |
Hyp |
Ref |
Expression |
1 |
|
odf1.1 |
|- X = ( Base ` G ) |
2 |
|
odf1.2 |
|- O = ( od ` G ) |
3 |
|
odf1.3 |
|- .x. = ( .g ` G ) |
4 |
|
odf1.4 |
|- F = ( x e. ZZ |-> ( x .x. A ) ) |
5 |
|
znnen |
|- ZZ ~~ NN |
6 |
|
nnenom |
|- NN ~~ _om |
7 |
5 6
|
entr2i |
|- _om ~~ ZZ |
8 |
1 2 3 4
|
odf1 |
|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 <-> F : ZZ -1-1-> X ) ) |
9 |
8
|
biimp3a |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> F : ZZ -1-1-> X ) |
10 |
|
f1f |
|- ( F : ZZ -1-1-> X -> F : ZZ --> X ) |
11 |
|
zex |
|- ZZ e. _V |
12 |
1
|
fvexi |
|- X e. _V |
13 |
|
fex2 |
|- ( ( F : ZZ --> X /\ ZZ e. _V /\ X e. _V ) -> F e. _V ) |
14 |
11 12 13
|
mp3an23 |
|- ( F : ZZ --> X -> F e. _V ) |
15 |
9 10 14
|
3syl |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> F e. _V ) |
16 |
|
f1f1orn |
|- ( F : ZZ -1-1-> X -> F : ZZ -1-1-onto-> ran F ) |
17 |
9 16
|
syl |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> F : ZZ -1-1-onto-> ran F ) |
18 |
|
f1oen3g |
|- ( ( F e. _V /\ F : ZZ -1-1-onto-> ran F ) -> ZZ ~~ ran F ) |
19 |
15 17 18
|
syl2anc |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ZZ ~~ ran F ) |
20 |
|
entr |
|- ( ( _om ~~ ZZ /\ ZZ ~~ ran F ) -> _om ~~ ran F ) |
21 |
7 19 20
|
sylancr |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> _om ~~ ran F ) |
22 |
|
endom |
|- ( _om ~~ ran F -> _om ~<_ ran F ) |
23 |
|
domnsym |
|- ( _om ~<_ ran F -> -. ran F ~< _om ) |
24 |
21 22 23
|
3syl |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ran F ~< _om ) |
25 |
|
isfinite |
|- ( ran F e. Fin <-> ran F ~< _om ) |
26 |
24 25
|
sylnibr |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ran F e. Fin ) |