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 ..^ 𝑁 ) ) )