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

Definition df-acs 13814
 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 7598 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 Moore
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-acs
StepHypRef Expression
1 cacs 13810 . 2 ACS
2 vx . . 3
3 cvv 2956 . . 3
42cv 1651 . . . . . . . 8
54cpw 3799 . . . . . . 7
6 vf . . . . . . . 8
76cv 1651 . . . . . . 7
85, 5, 7wf 5450 . . . . . 6
9 vs . . . . . . . . 9
10 vc . . . . . . . . 9
119, 10wel 1726 . . . . . . . 8
129cv 1651 . . . . . . . . . . . . 13
1312cpw 3799 . . . . . . . . . . . 12
14 cfn 7109 . . . . . . . . . . . 12
1513, 14cin 3319 . . . . . . . . . . 11
167, 15cima 4881 . . . . . . . . . 10
1716cuni 4015 . . . . . . . . 9
1817, 12wss 3320 . . . . . . . 8
1911, 18wb 177 . . . . . . 7
2019, 9, 5wral 2705 . . . . . 6
218, 20wa 359 . . . . 5
2221, 6wex 1550 . . . 4
23 cmre 13807 . . . . 5 Moore
244, 23cfv 5454 . . . 4 Moore
2522, 10, 24crab 2709 . . 3 Moore
262, 3, 25cmpt 4266 . 2 Moore
271, 26wceq 1652 1 ACS Moore
 Colors of variables: wff set class This definition is referenced by:  isacs  13876
 Copyright terms: Public domain W3C validator