Theorem naryfvalelwrdf

Description: An n-ary (endo)function on a set X expressed as a function over the set of words on X of length n . (Contributed by AV, 4-Jun-2024)

	Ref	Expression
Assertion	naryfvalelwrdf	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ↔ 𝐹 : { 𝑤 ∈ Word 𝑋 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ⟶ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
2	1	naryfvalel	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m ( 0 ..^ 𝑁 ) ) ⟶ 𝑋 ) )
3		wrdnval	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → { 𝑤 ∈ Word 𝑋 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ( 𝑋 ↑m ( 0 ..^ 𝑁 ) ) )
4	3	ancoms	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → { 𝑤 ∈ Word 𝑋 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ( 𝑋 ↑m ( 0 ..^ 𝑁 ) ) )
5	4	feq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 : { 𝑤 ∈ Word 𝑋 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ⟶ 𝑋 ↔ 𝐹 : ( 𝑋 ↑m ( 0 ..^ 𝑁 ) ) ⟶ 𝑋 ) )
6	2 5	bitr4d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ↔ 𝐹 : { 𝑤 ∈ Word 𝑋 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ⟶ 𝑋 ) )