Step |
Hyp |
Ref |
Expression |
1 |
|
hashwrdn |
|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` { w e. Word V | ( # ` w ) = N } ) = ( ( # ` V ) ^ N ) ) |
2 |
|
hashcl |
|- ( V e. Fin -> ( # ` V ) e. NN0 ) |
3 |
|
nn0expcl |
|- ( ( ( # ` V ) e. NN0 /\ N e. NN0 ) -> ( ( # ` V ) ^ N ) e. NN0 ) |
4 |
2 3
|
sylan |
|- ( ( V e. Fin /\ N e. NN0 ) -> ( ( # ` V ) ^ N ) e. NN0 ) |
5 |
1 4
|
eqeltrd |
|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` { w e. Word V | ( # ` w ) = N } ) e. NN0 ) |
6 |
5
|
ex |
|- ( V e. Fin -> ( N e. NN0 -> ( # ` { w e. Word V | ( # ` w ) = N } ) e. NN0 ) ) |
7 |
|
lencl |
|- ( w e. Word V -> ( # ` w ) e. NN0 ) |
8 |
|
eleq1 |
|- ( ( # ` w ) = N -> ( ( # ` w ) e. NN0 <-> N e. NN0 ) ) |
9 |
7 8
|
syl5ibcom |
|- ( w e. Word V -> ( ( # ` w ) = N -> N e. NN0 ) ) |
10 |
9
|
con3rr3 |
|- ( -. N e. NN0 -> ( w e. Word V -> -. ( # ` w ) = N ) ) |
11 |
10
|
ralrimiv |
|- ( -. N e. NN0 -> A. w e. Word V -. ( # ` w ) = N ) |
12 |
|
rabeq0 |
|- ( { w e. Word V | ( # ` w ) = N } = (/) <-> A. w e. Word V -. ( # ` w ) = N ) |
13 |
11 12
|
sylibr |
|- ( -. N e. NN0 -> { w e. Word V | ( # ` w ) = N } = (/) ) |
14 |
13
|
fveq2d |
|- ( -. N e. NN0 -> ( # ` { w e. Word V | ( # ` w ) = N } ) = ( # ` (/) ) ) |
15 |
|
hash0 |
|- ( # ` (/) ) = 0 |
16 |
14 15
|
eqtrdi |
|- ( -. N e. NN0 -> ( # ` { w e. Word V | ( # ` w ) = N } ) = 0 ) |
17 |
|
0nn0 |
|- 0 e. NN0 |
18 |
16 17
|
eqeltrdi |
|- ( -. N e. NN0 -> ( # ` { w e. Word V | ( # ` w ) = N } ) e. NN0 ) |
19 |
6 18
|
pm2.61d1 |
|- ( V e. Fin -> ( # ` { w e. Word V | ( # ` w ) = N } ) e. NN0 ) |
20 |
|
wrdexg |
|- ( V e. Fin -> Word V e. _V ) |
21 |
|
rabexg |
|- ( Word V e. _V -> { w e. Word V | ( # ` w ) = N } e. _V ) |
22 |
|
hashclb |
|- ( { w e. Word V | ( # ` w ) = N } e. _V -> ( { w e. Word V | ( # ` w ) = N } e. Fin <-> ( # ` { w e. Word V | ( # ` w ) = N } ) e. NN0 ) ) |
23 |
20 21 22
|
3syl |
|- ( V e. Fin -> ( { w e. Word V | ( # ` w ) = N } e. Fin <-> ( # ` { w e. Word V | ( # ` w ) = N } ) e. NN0 ) ) |
24 |
19 23
|
mpbird |
|- ( V e. Fin -> { w e. Word V | ( # ` w ) = N } e. Fin ) |