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 16072
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 8423 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 16068 . 2 class ACS
2 vx . . 3 setvar 𝑥
3 cvv 3173 . . 3 class V
42cv 1474 . . . . . . . 8 class 𝑥
54cpw 4108 . . . . . . 7 class 𝒫 𝑥
6 vf . . . . . . . 8 setvar 𝑓
76cv 1474 . . . . . . 7 class 𝑓
85, 5, 7wf 5800 . . . . . 6 wff 𝑓:𝒫 𝑥⟶𝒫 𝑥
9 vs . . . . . . . . 9 setvar 𝑠
10 vc . . . . . . . . 9 setvar 𝑐
119, 10wel 1978 . . . . . . . 8 wff 𝑠𝑐
129cv 1474 . . . . . . . . . . . . 13 class 𝑠
1312cpw 4108 . . . . . . . . . . . 12 class 𝒫 𝑠
14 cfn 7841 . . . . . . . . . . . 12 class Fin
1513, 14cin 3539 . . . . . . . . . . 11 class (𝒫 𝑠 ∩ Fin)
167, 15cima 5041 . . . . . . . . . 10 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
1716cuni 4372 . . . . . . . . 9 class (𝑓 “ (𝒫 𝑠 ∩ Fin))
1817, 12wss 3540 . . . . . . . 8 wff (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠
1911, 18wb 195 . . . . . . 7 wff (𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
2019, 9, 5wral 2896 . . . . . 6 wff 𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)
218, 20wa 383 . . . . 5 wff (𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
2221, 6wex 1695 . . . 4 wff 𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))
23 cmre 16065 . . . . 5 class Moore
244, 23cfv 5804 . . . 4 class (Moore‘𝑥)
2522, 10, 24crab 2900 . . 3 class {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}
262, 3, 25cmpt 4643 . 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
271, 26wceq 1475 1 wff ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
Colors of variables: wff setvar class
This definition is referenced by:  isacs  16135
  Copyright terms: Public domain W3C validator