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

Definition df-acs 13363
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 7228 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 13360 . 2  class ACS
2 vx . . 3  set  x
3 cvv 2727 . . 3  class  _V
42cv 1618 . . . . . . . 8  class  x
54cpw 3530 . . . . . . 7  class  ~P x
6 vf . . . . . . . 8  set  f
76cv 1618 . . . . . . 7  class  f
85, 5, 7wf 4588 . . . . . 6  wff  f : ~P x --> ~P x
9 vs . . . . . . . . 9  set  s
10 vc . . . . . . . . 9  set  c
119, 10wel 1622 . . . . . . . 8  wff  s  e.  c
129cv 1618 . . . . . . . . . . . . 13  class  s
1312cpw 3530 . . . . . . . . . . . 12  class  ~P s
14 cfn 6749 . . . . . . . . . . . 12  class  Fin
1513, 14cin 3077 . . . . . . . . . . 11  class  ( ~P s  i^i  Fin )
167, 15cima 4583 . . . . . . . . . 10  class  ( f
" ( ~P s  i^i  Fin ) )
1716cuni 3727 . . . . . . . . 9  class  U. (
f " ( ~P s  i^i  Fin )
)
1817, 12wss 3078 . . . . . . . 8  wff  U. (
f " ( ~P s  i^i  Fin )
)  C_  s
1911, 18wb 178 . . . . . . 7  wff  ( s  e.  c  <->  U. (
f " ( ~P s  i^i  Fin )
)  C_  s )
2019, 9, 5wral 2509 . . . . . 6  wff  A. s  e.  ~P  x ( s  e.  c  <->  U. (
f " ( ~P s  i^i  Fin )
)  C_  s )
218, 20wa 360 . . . . 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 1537 . . . 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 13358 . . . . 5  class Moore
244, 23cfv 4592 . . . 4  class  (Moore `  x )
2522, 10, 24crab 2512 . . 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 3974 . 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 1619 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  13398
  Copyright terms: Public domain W3C validator