Theorem wrdmap

Description: Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Assertion	wrdmap	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ↔ 𝑊 ∈ ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) = 𝑁 ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
2	1	elrab	⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
3		wrdnval	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) )
4	3	eleq2d	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ↔ 𝑊 ∈ ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) ) )
5	2 4	bitr3id	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ↔ 𝑊 ∈ ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) ) )