Definition df-naryf 47313

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

Assertion

Ref	Expression
df-naryf	⊢ -aryF = (𝑛 ∈ ℕ0, 𝑥 ∈ V ↦ (𝑥 ↑m (𝑥 ↑m (0..^𝑛))))

Distinct variable group:   𝑥,𝑛

Detailed syntax breakdown of Definition df-naryf

Step	Hyp	Ref	Expression
1		cnaryf 47312	. 2 class -aryF
2		vn	. . 3 setvar 𝑛
3		vx	. . 3 setvar 𝑥
4		cn0 12472	. . 3 class ℕ0
5		cvv 3475	. . 3 class V
6	3	cv 1541	. . . 4 class 𝑥
7		cc0 11110	. . . . . 6 class 0
8	2	cv 1541	. . . . . 6 class 𝑛
9		cfzo 13627	. . . . . 6 class ..^
10	7, 8, 9	co 7409	. . . . 5 class (0..^𝑛)
11		cmap 8820	. . . . 5 class ↑m
12	6, 10, 11	co 7409	. . . 4 class (𝑥 ↑m (0..^𝑛))
13	6, 12, 11	co 7409	. . 3 class (𝑥 ↑m (𝑥 ↑m (0..^𝑛)))
14	2, 3, 4, 5, 13	cmpo 7411	. 2 class (𝑛 ∈ ℕ0, 𝑥 ∈ V ↦ (𝑥 ↑m (𝑥 ↑m (0..^𝑛))))
15	1, 14	wceq 1542	1 wff -aryF = (𝑛 ∈ ℕ0, 𝑥 ∈ V ↦ (𝑥 ↑m (𝑥 ↑m (0..^𝑛))))

This definition is referenced by:  naryfval  47314  naryfvalixp  47315  naryrcl  47317  1aryenef  47331  2aryenef  47342