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	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in V\right)\to \left(F\in \left(N\mathrm{-aryF}X\right)\leftrightarrow F:\left\{w\in \mathrm{Word}X|\left|w\right|=N\right\}⟶X\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(0..^N\right)=\left(0..^N\right)$$
2	1	naryfvalel	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in V\right)\to \left(F\in \left(N\mathrm{-aryF}X\right)\leftrightarrow F:X^{\left(0..^N\right)}⟶X\right)$$
3		wrdnval	$$⊢\left(X\in V\wedge N\in {\mathbb{N}}_0\right)\to \left\{w\in \mathrm{Word}X|\left|w\right|=N\right\}=X^{\left(0..^N\right)}$$
4	3	ancoms	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in V\right)\to \left\{w\in \mathrm{Word}X|\left|w\right|=N\right\}=X^{\left(0..^N\right)}$$
5	4	feq2d	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in V\right)\to \left(F:\left\{w\in \mathrm{Word}X|\left|w\right|=N\right\}⟶X\leftrightarrow F:X^{\left(0..^N\right)}⟶X\right)$$
6	2 5	bitr4d	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in V\right)\to \left(F\in \left(N\mathrm{-aryF}X\right)\leftrightarrow F:\left\{w\in \mathrm{Word}X|\left|w\right|=N\right\}⟶X\right)$$