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 17537
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 9640 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 17533 . 2 class ACS
2 vx . . 3 setvar π‘₯
3 cvv 3474 . . 3 class V
42cv 1540 . . . . . . . 8 class π‘₯
54cpw 4602 . . . . . . 7 class 𝒫 π‘₯
6 vf . . . . . . . 8 setvar 𝑓
76cv 1540 . . . . . . 7 class 𝑓
85, 5, 7wf 6539 . . . . . 6 wff 𝑓:𝒫 π‘₯βŸΆπ’« π‘₯
9 vs . . . . . . . . 9 setvar 𝑠
10 vc . . . . . . . . 9 setvar 𝑐
119, 10wel 2107 . . . . . . . 8 wff 𝑠 ∈ 𝑐
129cv 1540 . . . . . . . . . . . . 13 class 𝑠
1312cpw 4602 . . . . . . . . . . . 12 class 𝒫 𝑠
14 cfn 8941 . . . . . . . . . . . 12 class Fin
1513, 14cin 3947 . . . . . . . . . . 11 class (𝒫 𝑠 ∩ Fin)
167, 15cima 5679 . . . . . . . . . 10 class (𝑓 β€œ (𝒫 𝑠 ∩ Fin))
1716cuni 4908 . . . . . . . . 9 class βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin))
1817, 12wss 3948 . . . . . . . 8 wff βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin)) βŠ† 𝑠
1911, 18wb 205 . . . . . . 7 wff (𝑠 ∈ 𝑐 ↔ βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin)) βŠ† 𝑠)
2019, 9, 5wral 3061 . . . . . 6 wff βˆ€π‘  ∈ 𝒫 π‘₯(𝑠 ∈ 𝑐 ↔ βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin)) βŠ† 𝑠)
218, 20wa 396 . . . . 5 wff (𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘  ∈ 𝒫 π‘₯(𝑠 ∈ 𝑐 ↔ βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin)) βŠ† 𝑠))
2221, 6wex 1781 . . . 4 wff βˆƒπ‘“(𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘  ∈ 𝒫 π‘₯(𝑠 ∈ 𝑐 ↔ βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin)) βŠ† 𝑠))
23 cmre 17530 . . . . 5 class Moore
244, 23cfv 6543 . . . 4 class (Mooreβ€˜π‘₯)
2522, 10, 24crab 3432 . . 3 class {𝑐 ∈ (Mooreβ€˜π‘₯) ∣ βˆƒπ‘“(𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘  ∈ 𝒫 π‘₯(𝑠 ∈ 𝑐 ↔ βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin)) βŠ† 𝑠))}
262, 3, 25cmpt 5231 . 2 class (π‘₯ ∈ V ↦ {𝑐 ∈ (Mooreβ€˜π‘₯) ∣ βˆƒπ‘“(𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘  ∈ 𝒫 π‘₯(𝑠 ∈ 𝑐 ↔ βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin)) βŠ† 𝑠))})
271, 26wceq 1541 1 wff ACS = (π‘₯ ∈ V ↦ {𝑐 ∈ (Mooreβ€˜π‘₯) ∣ βˆƒπ‘“(𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘  ∈ 𝒫 π‘₯(𝑠 ∈ 𝑐 ↔ βˆͺ (𝑓 β€œ (𝒫 𝑠 ∩ Fin)) βŠ† 𝑠))})
Colors of variables: wff setvar class
This definition is referenced by:  isacs  17599
  Copyright terms: Public domain W3C validator