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

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 eqabdv ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) = { 𝑤 ∣ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) } )
19 1 18 eqtr4id ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) )