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