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	Could not format assertion : No typesetting found for |- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : { w e. Word X | ( # ` w ) = N } --> X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(0..^N\right)=\left(0..^N\right)$$
2	1	naryfvalel	Could not format ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m ( 0 ..^ N ) ) --> X ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m ( 0 ..^ N ) ) --> X ) ) with typecode |-
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	Could not format ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : { w e. Word X | ( # ` w ) = N } --> X ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : { w e. Word X | ( # ` w ) = N } --> X ) ) with typecode |-