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