Metamath Proof Explorer


Theorem wrdnval

Description: Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Proof shortened by AV, 13-May-2020)

Ref Expression
Assertion wrdnval ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ( 𝑉m ( 0 ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 df-rab { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = { 𝑤 ∣ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) }
2 ovexd ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) → ( 0 ..^ 𝑁 ) ∈ V )
3 elmapg ( ( 𝑉𝑋 ∧ ( 0 ..^ 𝑁 ) ∈ V ) → ( 𝑤 ∈ ( 𝑉m ( 0 ..^ 𝑁 ) ) ↔ 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) )
4 2 3 syldan ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) → ( 𝑤 ∈ ( 𝑉m ( 0 ..^ 𝑁 ) ) ↔ 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) )
5 iswrdi ( 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉𝑤 ∈ Word 𝑉 )
6 5 adantl ( ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) ∧ 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) → 𝑤 ∈ Word 𝑉 )
7 fnfzo0hash ( ( 𝑁 ∈ ℕ0𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) → ( ♯ ‘ 𝑤 ) = 𝑁 )
8 7 adantll ( ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) ∧ 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) → ( ♯ ‘ 𝑤 ) = 𝑁 )
9 6 8 jca ( ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) ∧ 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) )
10 9 ex ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) → ( 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) ) )
11 wrdf ( 𝑤 ∈ Word 𝑉𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ 𝑉 )
12 oveq2 ( ( ♯ ‘ 𝑤 ) = 𝑁 → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ 𝑁 ) )
13 12 feq2d ( ( ♯ ‘ 𝑤 ) = 𝑁 → ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ 𝑉𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) )
14 11 13 syl5ibcom ( 𝑤 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑤 ) = 𝑁𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) )
15 14 imp ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) → 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )
16 10 15 impbid1 ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) → ( 𝑤 : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) ) )
17 4 16 bitrd ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) → ( 𝑤 ∈ ( 𝑉m ( 0 ..^ 𝑁 ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) ) )
18 17 abbi2dv ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) → ( 𝑉m ( 0 ..^ 𝑁 ) ) = { 𝑤 ∣ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) } )
19 1 18 eqtr4id ( ( 𝑉𝑋𝑁 ∈ ℕ0 ) → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ( 𝑉m ( 0 ..^ 𝑁 ) ) )