Definition df-naryf

Description: Define the n-ary (endo)functions. (Contributed by AV, 11-May-2024) (Revised by TA and SN, 7-Jun-2024)

	Ref	Expression
Assertion	df-naryf	Could not format assertion : No typesetting found for |- -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnaryf	Could not format -aryF : No typesetting found for class -aryF with typecode class
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vx	$$setvarx$$
4		cvv	$$class\mathrm{V}$$
5	3	cv	$$setvarx$$
6		cmap	$$class{\uparrow }_{𝑚}$$
7		cc0	$$class0$$
8		cfzo	$$class..^$$
9	1	cv	$$setvarn$$
10	7 9 8	co	$$class\left(0..^n\right)$$
11	5 10 6	co	$$class\left(x^{\left(0..^n\right)}\right)$$
12	5 11 6	co	$$class\left(x^{\left(x^{\left(0..^n\right)}\right)}\right)$$
13	1 3 2 4 12	cmpo	$$class\left(n\in {\mathbb{N}}_0,x\in \mathrm{V}⟼x^{\left(x^{\left(0..^n\right)}\right)}\right)$$
14	0 13	wceq	Could not format -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) : No typesetting found for wff -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) with typecode wff