This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )