Metamath Proof Explorer

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 = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnaryf 
 |-  -aryF
1 vn 
 |-  n
2 cn0 
 |-  NN0
3 vx 
 |-  x
4 cvv 
 |-  _V
5 3 cv 
 |-  x
6 cmap 
 |-  ^m
7 cc0 
 |-  0
8 cfzo 
 |-  ..^
9 1 cv 
 |-  n
10 7 9 8 co 
 |-  ( 0 ..^ n )
11 5 10 6 co 
 |-  ( x ^m ( 0 ..^ n ) )
12 5 11 6 co 
 |-  ( x ^m ( x ^m ( 0 ..^ n ) ) )
13 1 3 2 4 12 cmpo 
 |-  ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) )
14 0 13 wceq 
 |-  -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) )