Theorem naryrcl

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

	Ref	Expression
Hypothesis	naryfval.i	$$⊢I=\left(0..^N\right)$$
Assertion	naryrcl	Could not format assertion : No typesetting found for |- ( F e. ( N -aryF X ) -> ( N e. NN0 /\ X e. _V ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	$$⊢I=\left(0..^N\right)$$
2		df-naryf	Could not format -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) ) : No typesetting found for |- -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) ) with typecode |-
3	2	elmpocl	Could not format ( F e. ( N -aryF X ) -> ( N e. NN0 /\ X e. _V ) ) : No typesetting found for |- ( F e. ( N -aryF X ) -> ( N e. NN0 /\ X e. _V ) ) with typecode |-