Definition df-acs 17486

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 9528 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 17482	. 2 class ACS
2		vx	. . 3 setvar 𝑥
3		cvv 3436	. . 3 class V
4	2	cv 1540	. . . . . . . 8 class 𝑥
5	4	cpw 4545	. . . . . . 7 class 𝒫 𝑥
6		vf	. . . . . . . 8 setvar 𝑓
7	6	cv 1540	. . . . . . 7 class 𝑓
8	5, 5, 7	wf 6472	. . . . . 6 wff 𝑓:𝒫 𝑥⟶𝒫 𝑥
9		vs	. . . . . . . . 9 setvar 𝑠
10		vc	. . . . . . . . 9 setvar 𝑐
11	9, 10	wel 2112	. . . . . . . 8 wff 𝑠 ∈ 𝑐
12	9	cv 1540	. . . . . . . . . . . . 13 class 𝑠
13	12	cpw 4545	. . . . . . . . . . . 12 class 𝒫 𝑠
14		cfn 8864	. . . . . . . . . . . 12 class Fin
15	13, 14	cin 3896	. . . . . . . . . . 11 class (𝒫 𝑠 ∩ Fin)
16	7, 15	cima 5614	. . . . . . . . . 10 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
17	16	cuni 4854	. . . . . . . . 9 class ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin))
18	17, 12	wss 3897	. . . . . . . 8 wff ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠
19	11, 18	wb 206	. . . . . . 7 wff (𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
20	19, 9, 5	wral 3047	. . . . . 6 wff ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
21	8, 20	wa 395	. . . . 5 wff (𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
22	21, 6	wex 1780	. . . 4 wff ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
23		cmre 17479	. . . . 5 class Moore
24	4, 23	cfv 6476	. . . 4 class (Moore‘𝑥)
25	22, 10, 24	crab 3395	. . 3 class {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}
26	2, 3, 25	cmpt 5167	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
27	1, 26	wceq 1541	1 wff ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})

This definition is referenced by:  isacs  17552