Definition df-cloneop 35696

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 𝑎 to be a function on finite sequences of elements of 𝑎 (rather than tuples) with values in 𝑎. Following line 6 of [Szendrei] p. 11, the arity 𝑛 of an operation (here, the length of the sequences at which the operation is defined) is always finite and non-zero, whence 𝑛 is taken to be a non-zero finite ordinal. (Contributed by Adrian Ducourtial, 3-Apr-2025.)

Assertion

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

Distinct variable group:   𝑛,𝑎,𝑥

Detailed syntax breakdown of Definition df-cloneop

Step	Hyp	Ref	Expression
1		ccloneop 35695	. 2 class CloneOp
2		va	. . 3 setvar 𝑎
3		cvv 3480	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1539	. . . . . 6 class 𝑥
6	2	cv 1539	. . . . . . 7 class 𝑎
7		vn	. . . . . . . . 9 setvar 𝑛
8	7	cv 1539	. . . . . . . 8 class 𝑛
9		cmap 8866	. . . . . . . 8 class ↑m
10	6, 8, 9	co 7431	. . . . . . 7 class (𝑎 ↑m 𝑛)
11	6, 10, 9	co 7431	. . . . . 6 class (𝑎 ↑m (𝑎 ↑m 𝑛))
12	5, 11	wcel 2108	. . . . 5 wff 𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))
13		com 7887	. . . . . 6 class ω
14		c1o 8499	. . . . . 6 class 1o
15	13, 14	cdif 3948	. . . . 5 class (ω ∖ 1o)
16	12, 7, 15	wrex 3070	. . . 4 wff ∃𝑛 ∈ (ω ∖ 1o)𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))
17	16, 4	cab 2714	. . 3 class {𝑥 ∣ ∃𝑛 ∈ (ω ∖ 1o)𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))}
18	2, 3, 17	cmpt 5225	. 2 class (𝑎 ∈ V ↦ {𝑥 ∣ ∃𝑛 ∈ (ω ∖ 1o)𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))})
19	1, 18	wceq 1540	1 wff CloneOp = (𝑎 ∈ V ↦ {𝑥 ∣ ∃𝑛 ∈ (ω ∖ 1o)𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))})

This definition is referenced by: (None)