Metamath Proof Explorer

Definition df-acs

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 termedalgebraic 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 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion df-acs ⊢ ACS = x ∈ V ⟼ c ∈ Moore ⁡ x | ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s

Detailed syntax breakdown

Step Hyp Ref Expression
0 cacs class ACS
1 vx setvar x
2 cvv class V
3 vc setvar c
4 cmre class Moore
5 1 cv setvar x
6 5 4 cfv class Moore ⁡ x
7 vf setvar f
8 7 cv setvar f
9 5 cpw class 𝒫 x
10 9 9 8 wf wff f : 𝒫 x ⟶ 𝒫 x
11 vs setvar s
12 11 cv setvar s
13 3 cv setvar c
14 12 13 wcel wff s ∈ c
15 12 cpw class 𝒫 s
16 cfn class Fin
17 15 16 cin class 𝒫 s ∩ Fin
18 8 17 cima class f 𝒫 s ∩ Fin
19 18 cuni class ⋃ f 𝒫 s ∩ Fin
20 19 12 wss wff ⋃ f 𝒫 s ∩ Fin ⊆ s
21 14 20 wb wff s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
22 21 11 9 wral wff ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
23 10 22 wa wff f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
24 23 7 wex wff ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
25 24 3 6 crab class c ∈ Moore ⁡ x | ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
26 1 2 25 cmpt class x ∈ V ⟼ c ∈ Moore ⁡ x | ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
27 0 26 wceq wff ACS = x ∈ V ⟼ c ∈ Moore ⁡ x | ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s