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 = (a \in V ⟼ \{x \| \exists n \in (ω ∖ 1_{𝑜}) x \in (a^{(a^{n})})\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccloneop	$class CloneOp$
1		va	$setvar a$
2		cvv	$class V$
3		vx	$setvar x$
4		vn	$setvar n$
5		com	$class ω$
6		c1o	$class 1_{𝑜}$
7	5 6	cdif	$class (ω ∖ 1_{𝑜})$
8	3	cv	$setvar x$
9	1	cv	$setvar a$
10		cmap	$class ↑_{𝑚}$
11	4	cv	$setvar n$
12	9 11 10	co	$class (a^{n})$
13	9 12 10	co	$class (a^{(a^{n})})$
14	8 13	wcel	$wff x \in (a^{(a^{n})})$
15	14 4 7	wrex	$wff \exists n \in (ω ∖ 1_{𝑜}) x \in (a^{(a^{n})})$
16	15 3	cab	$class \{x \| \exists n \in (ω ∖ 1_{𝑜}) x \in (a^{(a^{n})})\}$
17	1 2 16	cmpt	$class (a \in V ⟼ \{x \| \exists n \in (ω ∖ 1_{𝑜}) x \in (a^{(a^{n})})\})$
18	0 17	wceq	$wff CloneOp = (a \in V ⟼ \{x \| \exists n \in (ω ∖ 1_{𝑜}) x \in (a^{(a^{n})})\})$

Metamath Proof Explorer

Definition df-cloneop

Detailed syntax breakdown