Step |
Hyp |
Ref |
Expression |
1 |
|
odhash.x |
|- X = ( Base ` G ) |
2 |
|
odhash.o |
|- O = ( od ` G ) |
3 |
|
odhash.k |
|- K = ( mrCls ` ( SubGrp ` G ) ) |
4 |
|
zex |
|- ZZ e. _V |
5 |
|
ominf |
|- -. _om e. Fin |
6 |
|
znnen |
|- ZZ ~~ NN |
7 |
|
nnenom |
|- NN ~~ _om |
8 |
6 7
|
entri |
|- ZZ ~~ _om |
9 |
|
enfi |
|- ( ZZ ~~ _om -> ( ZZ e. Fin <-> _om e. Fin ) ) |
10 |
8 9
|
ax-mp |
|- ( ZZ e. Fin <-> _om e. Fin ) |
11 |
5 10
|
mtbir |
|- -. ZZ e. Fin |
12 |
|
hashinf |
|- ( ( ZZ e. _V /\ -. ZZ e. Fin ) -> ( # ` ZZ ) = +oo ) |
13 |
4 11 12
|
mp2an |
|- ( # ` ZZ ) = +oo |
14 |
|
eqid |
|- ( .g ` G ) = ( .g ` G ) |
15 |
1 14 2 3
|
odf1o1 |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ -1-1-onto-> ( K ` { A } ) ) |
16 |
4
|
f1oen |
|- ( ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ -1-1-onto-> ( K ` { A } ) -> ZZ ~~ ( K ` { A } ) ) |
17 |
|
hasheni |
|- ( ZZ ~~ ( K ` { A } ) -> ( # ` ZZ ) = ( # ` ( K ` { A } ) ) ) |
18 |
15 16 17
|
3syl |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( # ` ZZ ) = ( # ` ( K ` { A } ) ) ) |
19 |
13 18
|
syl5reqr |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( # ` ( K ` { A } ) ) = +oo ) |