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 ) |