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

Definition df-acs 13806
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 7590 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  =  ( x  e.  _V  |->  { c  e.  (Moore `  x )  |  E. f ( f : ~P x --> ~P x  /\  A. s  e.  ~P  x ( s  e.  c  <->  U. ( f "
( ~P s  i^i 
Fin ) )  C_  s ) ) } )
Distinct variable group:    f, c, s, x

Detailed syntax breakdown of Definition df-acs
StepHypRef Expression
1 cacs 13802 . 2  class ACS
2 vx . . 3  set  x
3 cvv 2948 . . 3  class  _V
42cv 1651 . . . . . . . 8  class  x
54cpw 3791 . . . . . . 7  class  ~P x
6 vf . . . . . . . 8  set  f
76cv 1651 . . . . . . 7  class  f
85, 5, 7wf 5442 . . . . . 6  wff  f : ~P x --> ~P x
9 vs . . . . . . . . 9  set  s
10 vc . . . . . . . . 9  set  c
119, 10wel 1726 . . . . . . . 8  wff  s  e.  c
129cv 1651 . . . . . . . . . . . . 13  class  s
1312cpw 3791 . . . . . . . . . . . 12  class  ~P s
14 cfn 7101 . . . . . . . . . . . 12  class  Fin
1513, 14cin 3311 . . . . . . . . . . 11  class  ( ~P s  i^i  Fin )
167, 15cima 4873 . . . . . . . . . 10  class  ( f
" ( ~P s  i^i  Fin ) )
1716cuni 4007 . . . . . . . . 9  class  U. (
f " ( ~P s  i^i  Fin )
)
1817, 12wss 3312 . . . . . . . 8  wff  U. (
f " ( ~P s  i^i  Fin )
)  C_  s
1911, 18wb 177 . . . . . . 7  wff  ( s  e.  c  <->  U. (
f " ( ~P s  i^i  Fin )
)  C_  s )
2019, 9, 5wral 2697 . . . . . 6  wff  A. s  e.  ~P  x ( s  e.  c  <->  U. (
f " ( ~P s  i^i  Fin )
)  C_  s )
218, 20wa 359 . . . . 5  wff  ( f : ~P x --> ~P x  /\  A. s  e.  ~P  x ( s  e.  c  <->  U. ( f "
( ~P s  i^i 
Fin ) )  C_  s ) )
2221, 6wex 1550 . . . 4  wff  E. f
( f : ~P x
--> ~P x  /\  A. s  e.  ~P  x
( s  e.  c  <->  U. ( f " ( ~P s  i^i  Fin )
)  C_  s )
)
23 cmre 13799 . . . . 5  class Moore
244, 23cfv 5446 . . . 4  class  (Moore `  x )
2522, 10, 24crab 2701 . . 3  class  { c  e.  (Moore `  x
)  |  E. f
( f : ~P x
--> ~P x  /\  A. s  e.  ~P  x
( s  e.  c  <->  U. ( f " ( ~P s  i^i  Fin )
)  C_  s )
) }
262, 3, 25cmpt 4258 . 2  class  ( x  e.  _V  |->  { c  e.  (Moore `  x
)  |  E. f
( f : ~P x
--> ~P x  /\  A. s  e.  ~P  x
( s  e.  c  <->  U. ( f " ( ~P s  i^i  Fin )
)  C_  s )
) } )
271, 26wceq 1652 1  wff ACS  =  ( x  e.  _V  |->  { c  e.  (Moore `  x )  |  E. f ( f : ~P x --> ~P x  /\  A. s  e.  ~P  x ( s  e.  c  <->  U. ( f "
( ~P s  i^i 
Fin ) )  C_  s ) ) } )
Colors of variables: wff set class
This definition is referenced by:  isacs  13868
  Copyright terms: Public domain W3C validator