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 ( 𝑉 ∈ Fin → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ Fin )

Proof

Step Hyp Ref Expression
1 hashwrdn ( ( 𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) = ( ( ♯ ‘ 𝑉 ) ↑ 𝑁 ) )
2 hashcl ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
3 nn0expcl ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑉 ) ↑ 𝑁 ) ∈ ℕ0 )
4 2 3 sylan ( ( 𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑉 ) ↑ 𝑁 ) ∈ ℕ0 )
5 1 4 eqeltrd ( ( 𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) ∈ ℕ0 )
6 5 ex ( 𝑉 ∈ Fin → ( 𝑁 ∈ ℕ0 → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) ∈ ℕ0 ) )
7 lencl ( 𝑤 ∈ Word 𝑉 → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
8 eleq1 ( ( ♯ ‘ 𝑤 ) = 𝑁 → ( ( ♯ ‘ 𝑤 ) ∈ ℕ0𝑁 ∈ ℕ0 ) )
9 7 8 syl5ibcom ( 𝑤 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑤 ) = 𝑁𝑁 ∈ ℕ0 ) )
10 9 con3rr3 ( ¬ 𝑁 ∈ ℕ0 → ( 𝑤 ∈ Word 𝑉 → ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) )
11 10 ralrimiv ( ¬ 𝑁 ∈ ℕ0 → ∀ 𝑤 ∈ Word 𝑉 ¬ ( ♯ ‘ 𝑤 ) = 𝑁 )
12 rabeq0 ( { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ∅ ↔ ∀ 𝑤 ∈ Word 𝑉 ¬ ( ♯ ‘ 𝑤 ) = 𝑁 )
13 11 12 sylibr ( ¬ 𝑁 ∈ ℕ0 → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ∅ )
14 13 fveq2d ( ¬ 𝑁 ∈ ℕ0 → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) = ( ♯ ‘ ∅ ) )
15 hash0 ( ♯ ‘ ∅ ) = 0
16 14 15 eqtrdi ( ¬ 𝑁 ∈ ℕ0 → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) = 0 )
17 0nn0 0 ∈ ℕ0
18 16 17 eqeltrdi ( ¬ 𝑁 ∈ ℕ0 → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) ∈ ℕ0 )
19 6 18 pm2.61d1 ( 𝑉 ∈ Fin → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) ∈ ℕ0 )
20 wrdexg ( 𝑉 ∈ Fin → Word 𝑉 ∈ V )
21 rabexg ( Word 𝑉 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ V )
22 hashclb ( { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ V → ( { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ Fin ↔ ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) ∈ ℕ0 ) )
23 20 21 22 3syl ( 𝑉 ∈ Fin → ( { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ Fin ↔ ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) ∈ ℕ0 ) )
24 19 23 mpbird ( 𝑉 ∈ Fin → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ Fin )