Theorem naryrcl

Description: Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024)

	Ref	Expression
Hypothesis	naryfval.i	|- I = ( 0 ..^ N )
Assertion	naryrcl	|- ( F e. ( N -aryF X ) -> ( N e. NN0 /\ X e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	|- I = ( 0 ..^ N )
2		df-naryf	|- -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) )
3	2	elmpocl	|- ( F e. ( N -aryF X ) -> ( N e. NN0 /\ X e. _V ) )