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	⊢ -aryF = ( 𝑛 ∈ ℕ0 , 𝑥 ∈ V ↦ ( 𝑥 ↑m ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnaryf	⊢ -aryF
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vx	⊢ 𝑥
4		cvv	⊢ V
5	3	cv	⊢ 𝑥
6		cmap	⊢ ↑m
7		cc0	⊢ 0
8		cfzo	⊢ ..^
9	1	cv	⊢ 𝑛
10	7 9 8	co	⊢ ( 0 ..^ 𝑛 )
11	5 10 6	co	⊢ ( 𝑥 ↑m ( 0 ..^ 𝑛 ) )
12	5 11 6	co	⊢ ( 𝑥 ↑m ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) )
13	1 3 2 4 12	cmpo	⊢ ( 𝑛 ∈ ℕ0 , 𝑥 ∈ V ↦ ( 𝑥 ↑m ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) ) )
14	0 13	wceq	⊢ -aryF = ( 𝑛 ∈ ℕ0 , 𝑥 ∈ V ↦ ( 𝑥 ↑m ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) ) )