Definition df-acs 17633

Description: An important subclass of Moore systems are those which can be interpreted as closure under some collection of operators of finite arity (the collection itself is not required to be finite). These are termed algebraic closure systems; similar to definition (A) of an algebraic closure system in [Schechter] p. 84, but to avoid the complexity of an arbitrary mixed collection of functions of various arities (especially if the axiom of infinity omex 9680 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015.)

Assertion

Ref	Expression
df-acs	⊢ ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})

Distinct variable group:   𝑓,𝑐,𝑠,𝑥

Detailed syntax breakdown of Definition df-acs

Step	Hyp	Ref	Expression
1		cacs 17629	. 2 class ACS
2		vx	. . 3 setvar 𝑥
3		cvv 3477	. . 3 class V
4	2	cv 1535	. . . . . . . 8 class 𝑥
5	4	cpw 4604	. . . . . . 7 class 𝒫 𝑥
6		vf	. . . . . . . 8 setvar 𝑓
7	6	cv 1535	. . . . . . 7 class 𝑓
8	5, 5, 7	wf 6558	. . . . . 6 wff 𝑓:𝒫 𝑥⟶𝒫 𝑥
9		vs	. . . . . . . . 9 setvar 𝑠
10		vc	. . . . . . . . 9 setvar 𝑐
11	9, 10	wel 2106	. . . . . . . 8 wff 𝑠 ∈ 𝑐
12	9	cv 1535	. . . . . . . . . . . . 13 class 𝑠
13	12	cpw 4604	. . . . . . . . . . . 12 class 𝒫 𝑠
14		cfn 8983	. . . . . . . . . . . 12 class Fin
15	13, 14	cin 3961	. . . . . . . . . . 11 class (𝒫 𝑠 ∩ Fin)
16	7, 15	cima 5691	. . . . . . . . . 10 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
17	16	cuni 4911	. . . . . . . . 9 class ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin))
18	17, 12	wss 3962	. . . . . . . 8 wff ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠
19	11, 18	wb 206	. . . . . . 7 wff (𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
20	19, 9, 5	wral 3058	. . . . . 6 wff ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
21	8, 20	wa 395	. . . . 5 wff (𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
22	21, 6	wex 1775	. . . 4 wff ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
23		cmre 17626	. . . . 5 class Moore
24	4, 23	cfv 6562	. . . 4 class (Moore‘𝑥)
25	22, 10, 24	crab 3432	. . 3 class {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}
26	2, 3, 25	cmpt 5230	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
27	1, 26	wceq 1536	1 wff ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})

This definition is referenced by:  isacs  17695