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	$$⊢\mathrm{-aryF}=\left(n\in {\mathbb{N}}_0,x\in \mathrm{V}⟼x^{\left(x^{\left(0..^n\right)}\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnaryf	$$class\mathrm{-aryF}$$
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	$$wff\mathrm{-aryF}=\left(n\in {\mathbb{N}}_0,x\in \mathrm{V}⟼x^{\left(x^{\left(0..^n\right)}\right)}\right)$$