MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-acs Structured version   Visualization version   GIF version

Definition df-acs 17632
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 9683 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
StepHypRef Expression
1 cacs 17628 . 2 class ACS
2 vx . . 3 setvar 𝑥
3 cvv 3480 . . 3 class V
42cv 1539 . . . . . . . 8 class 𝑥
54cpw 4600 . . . . . . 7 class 𝒫 𝑥
6 vf . . . . . . . 8 setvar 𝑓
76cv 1539 . . . . . . 7 class 𝑓
85, 5, 7wf 6557 . . . . . 6 wff 𝑓:𝒫 𝑥⟶𝒫 𝑥
9 vs . . . . . . . . 9 setvar 𝑠
10 vc . . . . . . . . 9 setvar 𝑐
119, 10wel 2109 . . . . . . . 8 wff 𝑠𝑐
129cv 1539 . . . . . . . . . . . . 13 class 𝑠
1312cpw 4600 . . . . . . . . . . . 12 class 𝒫 𝑠
14 cfn 8985 . . . . . . . . . . . 12 class Fin
1513, 14cin 3950 . . . . . . . . . . 11 class (𝒫 𝑠 ∩ Fin)
167, 15cima 5688 . . . . . . . . . 10 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
1716cuni 4907 . . . . . . . . 9 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
1817, 12wss 3951 . . . . . . . 8 wff (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠
1911, 18wb 206 . . . . . . 7 wff (𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
2019, 9, 5wral 3061 . . . . . 6 wff 𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
218, 20wa 395 . . . . 5 wff (𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
2221, 6wex 1779 . . . 4 wff 𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
23 cmre 17625 . . . . 5 class Moore
244, 23cfv 6561 . . . 4 class (Moore‘𝑥)
2522, 10, 24crab 3436 . . 3 class {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}
262, 3, 25cmpt 5225 . 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
271, 26wceq 1540 1 wff ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
Colors of variables: wff setvar class
This definition is referenced by:  isacs  17694
  Copyright terms: Public domain W3C validator