Definition df-acs 17533

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 9638 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 17529	. 2 class ACS
2		vx	. . 3 setvar 𝑥
3		cvv 3475	. . 3 class V
4	2	cv 1541	. . . . . . . 8 class 𝑥
5	4	cpw 4603	. . . . . . 7 class 𝒫 𝑥
6		vf	. . . . . . . 8 setvar 𝑓
7	6	cv 1541	. . . . . . 7 class 𝑓
8	5, 5, 7	wf 6540	. . . . . 6 wff 𝑓:𝒫 𝑥⟶𝒫 𝑥
9		vs	. . . . . . . . 9 setvar 𝑠
10		vc	. . . . . . . . 9 setvar 𝑐
11	9, 10	wel 2108	. . . . . . . 8 wff 𝑠 ∈ 𝑐
12	9	cv 1541	. . . . . . . . . . . . 13 class 𝑠
13	12	cpw 4603	. . . . . . . . . . . 12 class 𝒫 𝑠
14		cfn 8939	. . . . . . . . . . . 12 class Fin
15	13, 14	cin 3948	. . . . . . . . . . 11 class (𝒫 𝑠 ∩ Fin)
16	7, 15	cima 5680	. . . . . . . . . 10 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
17	16	cuni 4909	. . . . . . . . 9 class ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin))
18	17, 12	wss 3949	. . . . . . . 8 wff ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠
19	11, 18	wb 205	. . . . . . 7 wff (𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
20	19, 9, 5	wral 3062	. . . . . 6 wff ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
21	8, 20	wa 397	. . . . 5 wff (𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
22	21, 6	wex 1782	. . . 4 wff ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
23		cmre 17526	. . . . 5 class Moore
24	4, 23	cfv 6544	. . . 4 class (Moore‘𝑥)
25	22, 10, 24	crab 3433	. . 3 class {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}
26	2, 3, 25	cmpt 5232	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
27	1, 26	wceq 1542	1 wff ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})

This definition is referenced by:  isacs  17595