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 ∈ Fin → w ∈ Word V | w = N ∈ Fin

Proof

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