Metamath Proof Explorer


Theorem wrdnfi

Description: If there is only a finite number of symbols, the number of words of a fixed length over these symbols is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018) Remove unnecessary antecedent. (Revised by JJ, 18-Nov-2022)

Ref Expression
Assertion wrdnfi
|- ( V e. Fin -> { w e. Word V | ( # ` w ) = N } e. Fin )

Proof

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 )