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 )