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

Definition df-acs 14519
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 7841 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
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-acs
StepHypRef Expression
1 cacs 14515 . 2
2 vx . . 3
3 cvv 2967 . . 3
42cv 1368 . . . . . . . 8
54cpw 3855 . . . . . . 7
6 vf . . . . . . . 8
76cv 1368 . . . . . . 7
85, 5, 7wf 5409 . . . . . 6
9 vs . . . . . . . . 9
10 vc . . . . . . . . 9
119, 10wel 1757 . . . . . . . 8
129cv 1368 . . . . . . . . . . . . 13
1312cpw 3855 . . . . . . . . . . . 12
14 cfn 7302 . . . . . . . . . . . 12
1513, 14cin 3322 . . . . . . . . . . 11
167, 15cima 4838 . . . . . . . . . 10
1716cuni 4086 . . . . . . . . 9
1817, 12wss 3323 . . . . . . . 8
1911, 18wb 184 . . . . . . 7
2019, 9, 5wral 2710 . . . . . 6
218, 20wa 369 . . . . 5
2221, 6wex 1586 . . . 4
23 cmre 14512 . . . . 5
244, 23cfv 5413 . . . 4
2522, 10, 24crab 2714 . . 3
262, 3, 25cmpt 4345 . 2
271, 26wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  isacs  14581
  Copyright terms: Public domain W3C validator