Definition df-cloneop

Description: Define the function that sends a set to the class of clone-theoretic operations on the set. For convenience, we take an operation on a to be a function on finite sequences of elements of a (rather than tuples) with values in a . Following line 6 of Szendrei p. 11, the arity n of an operation (here, the length of the sequences at which the operation is defined) is always finite and non-zero, whence n is taken to be a non-zero finite ordinal. (Contributed by Adrian Ducourtial, 3-Apr-2025)

	Ref	Expression
Assertion	df-cloneop	|- CloneOp = ( a e. _V |-> { x | E. n e. ( _om \ 1o ) x e. ( a ^m ( a ^m n ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccloneop	|- CloneOp
1		va	|- a
2		cvv	|- _V
3		vx	|- x
4		vn	|- n
5		com	|- _om
6		c1o	|- 1o
7	5 6	cdif	|- ( _om \ 1o )
8	3	cv	|- x
9	1	cv	|- a
10		cmap	|- ^m
11	4	cv	|- n
12	9 11 10	co	|- ( a ^m n )
13	9 12 10	co	|- ( a ^m ( a ^m n ) )
14	8 13	wcel	|- x e. ( a ^m ( a ^m n ) )
15	14 4 7	wrex	|- E. n e. ( _om \ 1o ) x e. ( a ^m ( a ^m n ) )
16	15 3	cab	|- { x | E. n e. ( _om \ 1o ) x e. ( a ^m ( a ^m n ) ) }
17	1 2 16	cmpt	|- ( a e. _V |-> { x | E. n e. ( _om \ 1o ) x e. ( a ^m ( a ^m n ) ) } )
18	0 17	wceq	|- CloneOp = ( a e. _V |-> { x | E. n e. ( _om \ 1o ) x e. ( a ^m ( a ^m n ) ) } )