Step |
Hyp |
Ref |
Expression |
1 |
|
wrdnval |
|- ( ( V e. Fin /\ N e. NN0 ) -> { w e. Word V | ( # ` w ) = N } = ( V ^m ( 0 ..^ N ) ) ) |
2 |
1
|
fveq2d |
|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` { w e. Word V | ( # ` w ) = N } ) = ( # ` ( V ^m ( 0 ..^ N ) ) ) ) |
3 |
|
fzofi |
|- ( 0 ..^ N ) e. Fin |
4 |
|
hashmap |
|- ( ( V e. Fin /\ ( 0 ..^ N ) e. Fin ) -> ( # ` ( V ^m ( 0 ..^ N ) ) ) = ( ( # ` V ) ^ ( # ` ( 0 ..^ N ) ) ) ) |
5 |
3 4
|
mpan2 |
|- ( V e. Fin -> ( # ` ( V ^m ( 0 ..^ N ) ) ) = ( ( # ` V ) ^ ( # ` ( 0 ..^ N ) ) ) ) |
6 |
|
hashfzo0 |
|- ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N ) |
7 |
6
|
oveq2d |
|- ( N e. NN0 -> ( ( # ` V ) ^ ( # ` ( 0 ..^ N ) ) ) = ( ( # ` V ) ^ N ) ) |
8 |
5 7
|
sylan9eq |
|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` ( V ^m ( 0 ..^ N ) ) ) = ( ( # ` V ) ^ N ) ) |
9 |
2 8
|
eqtrd |
|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` { w e. Word V | ( # ` w ) = N } ) = ( ( # ` V ) ^ N ) ) |