Definition df-acs 17215

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 9331 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 17211	. 2 class ACS
2		vx	. . 3 setvar 𝑥
3		cvv 3422	. . 3 class V
4	2	cv 1538	. . . . . . . 8 class 𝑥
5	4	cpw 4530	. . . . . . 7 class 𝒫 𝑥
6		vf	. . . . . . . 8 setvar 𝑓
7	6	cv 1538	. . . . . . 7 class 𝑓
8	5, 5, 7	wf 6414	. . . . . 6 wff 𝑓:𝒫 𝑥⟶𝒫 𝑥
9		vs	. . . . . . . . 9 setvar 𝑠
10		vc	. . . . . . . . 9 setvar 𝑐
11	9, 10	wel 2109	. . . . . . . 8 wff 𝑠 ∈ 𝑐
12	9	cv 1538	. . . . . . . . . . . . 13 class 𝑠
13	12	cpw 4530	. . . . . . . . . . . 12 class 𝒫 𝑠
14		cfn 8691	. . . . . . . . . . . 12 class Fin
15	13, 14	cin 3882	. . . . . . . . . . 11 class (𝒫 𝑠 ∩ Fin)
16	7, 15	cima 5583	. . . . . . . . . 10 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
17	16	cuni 4836	. . . . . . . . 9 class ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin))
18	17, 12	wss 3883	. . . . . . . 8 wff ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠
19	11, 18	wb 205	. . . . . . 7 wff (𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
20	19, 9, 5	wral 3063	. . . . . 6 wff ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
21	8, 20	wa 395	. . . . 5 wff (𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
22	21, 6	wex 1783	. . . 4 wff ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
23		cmre 17208	. . . . 5 class Moore
24	4, 23	cfv 6418	. . . 4 class (Moore‘𝑥)
25	22, 10, 24	crab 3067	. . 3 class {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}
26	2, 3, 25	cmpt 5153	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
27	1, 26	wceq 1539	1 wff ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})

This definition is referenced by:  isacs  17277