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 nonzero, whence n is taken to be a nonzero finite ordinal. (Contributed by Adrian Ducourtial, 3-Apr-2025)

	Ref	Expression
Assertion	df-cloneop	⊢ CloneOp = ( 𝑎 ∈ V ↦ { 𝑥 ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) 𝑥 ∈ ( 𝑎 ↑m ( 𝑎 ↑m 𝑛 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccloneop	⊢ CloneOp
1		va	⊢ 𝑎
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		vn	⊢ 𝑛
5		com	⊢ ω
6		c1o	⊢ 1o
7	5 6	cdif	⊢ ( ω ∖ 1o )
8	3	cv	⊢ 𝑥
9	1	cv	⊢ 𝑎
10		cmap	⊢ ↑m
11	4	cv	⊢ 𝑛
12	9 11 10	co	⊢ ( 𝑎 ↑m 𝑛 )
13	9 12 10	co	⊢ ( 𝑎 ↑m ( 𝑎 ↑m 𝑛 ) )
14	8 13	wcel	⊢ 𝑥 ∈ ( 𝑎 ↑m ( 𝑎 ↑m 𝑛 ) )
15	14 4 7	wrex	⊢ ∃ 𝑛 ∈ ( ω ∖ 1o ) 𝑥 ∈ ( 𝑎 ↑m ( 𝑎 ↑m 𝑛 ) )
16	15 3	cab	⊢ { 𝑥 ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) 𝑥 ∈ ( 𝑎 ↑m ( 𝑎 ↑m 𝑛 ) ) }
17	1 2 16	cmpt	⊢ ( 𝑎 ∈ V ↦ { 𝑥 ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) 𝑥 ∈ ( 𝑎 ↑m ( 𝑎 ↑m 𝑛 ) ) } )
18	0 17	wceq	⊢ CloneOp = ( 𝑎 ∈ V ↦ { 𝑥 ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) 𝑥 ∈ ( 𝑎 ↑m ( 𝑎 ↑m 𝑛 ) ) } )