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	|- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : { w e. Word X | ( # ` w ) = N } --> X ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( 0 ..^ N ) = ( 0 ..^ N )
2	1	naryfvalel	|- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m ( 0 ..^ N ) ) --> X ) )
3		wrdnval	|- ( ( X e. V /\ N e. NN0 ) -> { w e. Word X | ( # ` w ) = N } = ( X ^m ( 0 ..^ N ) ) )
4	3	ancoms	|- ( ( N e. NN0 /\ X e. V ) -> { w e. Word X | ( # ` w ) = N } = ( X ^m ( 0 ..^ N ) ) )
5	4	feq2d	|- ( ( N e. NN0 /\ X e. V ) -> ( F : { w e. Word X | ( # ` w ) = N } --> X <-> F : ( X ^m ( 0 ..^ N ) ) --> X ) )
6	2 5	bitr4d	|- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : { w e. Word X | ( # ` w ) = N } --> X ) )