Definition df-acs 17483

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 9588 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 17479	. 2 class ACS
2		vx	. . 3 setvar 𝑥
3		cvv 3446	. . 3 class V
4	2	cv 1540	. . . . . . . 8 class 𝑥
5	4	cpw 4565	. . . . . . 7 class 𝒫 𝑥
6		vf	. . . . . . . 8 setvar 𝑓
7	6	cv 1540	. . . . . . 7 class 𝑓
8	5, 5, 7	wf 6497	. . . . . 6 wff 𝑓:𝒫 𝑥⟶𝒫 𝑥
9		vs	. . . . . . . . 9 setvar 𝑠
10		vc	. . . . . . . . 9 setvar 𝑐
11	9, 10	wel 2107	. . . . . . . 8 wff 𝑠 ∈ 𝑐
12	9	cv 1540	. . . . . . . . . . . . 13 class 𝑠
13	12	cpw 4565	. . . . . . . . . . . 12 class 𝒫 𝑠
14		cfn 8890	. . . . . . . . . . . 12 class Fin
15	13, 14	cin 3912	. . . . . . . . . . 11 class (𝒫 𝑠 ∩ Fin)
16	7, 15	cima 5641	. . . . . . . . . 10 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
17	16	cuni 4870	. . . . . . . . 9 class ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin))
18	17, 12	wss 3913	. . . . . . . 8 wff ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠
19	11, 18	wb 205	. . . . . . 7 wff (𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
20	19, 9, 5	wral 3060	. . . . . 6 wff ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
21	8, 20	wa 396	. . . . 5 wff (𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
22	21, 6	wex 1781	. . . 4 wff ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
23		cmre 17476	. . . . 5 class Moore
24	4, 23	cfv 6501	. . . 4 class (Moore‘𝑥)
25	22, 10, 24	crab 3405	. . 3 class {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}
26	2, 3, 25	cmpt 5193	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
27	1, 26	wceq 1541	1 wff ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})

This definition is referenced by:  isacs  17545