Theorem naryfvalel

Description: An n-ary (endo)function on a set X . (Contributed by AV, 14-May-2024)

	Ref	Expression
Hypothesis	naryfval.i	$$⊢I=\left(0..^N\right)$$
Assertion	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^I⟶X\right)$$

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	$$⊢I=\left(0..^N\right)$$
2	1	naryfval	$$⊢N\in {\mathbb{N}}_0\to N\mathrm{-aryF}X=X^{\left(X^I\right)}$$
3	2	eleq2d	$$⊢N\in {\mathbb{N}}_0\to \left(F\in \left(N\mathrm{-aryF}X\right)\leftrightarrow F\in \left(X^{\left(X^I\right)}\right)\right)$$
4		ovex	$$⊢X^I\in \mathrm{V}$$
5		elmapg	$$⊢\left(X\in V\wedge X^I\in \mathrm{V}\right)\to \left(F\in \left(X^{\left(X^I\right)}\right)\leftrightarrow F:X^I⟶X\right)$$
6	4 5	mpan2	$$⊢X\in V\to \left(F\in \left(X^{\left(X^I\right)}\right)\leftrightarrow F:X^I⟶X\right)$$
7	3 6	sylan9bb	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in V\right)\to \left(F\in \left(N\mathrm{-aryF}X\right)\leftrightarrow F:X^I⟶X\right)$$