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

Definition df-acs 13493
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 7346 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 13489 . 2  class ACS
2 vx . . 3  set  x
3 cvv 2790 . . 3  class  _V
42cv 1624 . . . . . . . 8  class  x
54cpw 3627 . . . . . . 7  class  ~P x
6 vf . . . . . . . 8  set  f
76cv 1624 . . . . . . 7  class  f
85, 5, 7wf 5253 . . . . . 6  wff  f : ~P x --> ~P x
9 vs . . . . . . . . 9  set  s
10 vc . . . . . . . . 9  set  c
119, 10wel 1687 . . . . . . . 8  wff  s  e.  c
129cv 1624 . . . . . . . . . . . . 13  class  s
1312cpw 3627 . . . . . . . . . . . 12  class  ~P s
14 cfn 6865 . . . . . . . . . . . 12  class  Fin
1513, 14cin 3153 . . . . . . . . . . 11  class  ( ~P s  i^i  Fin )
167, 15cima 4694 . . . . . . . . . 10  class  ( f
" ( ~P s  i^i  Fin ) )
1716cuni 3829 . . . . . . . . 9  class  U. (
f " ( ~P s  i^i  Fin )
)
1817, 12wss 3154 . . . . . . . 8  wff  U. (
f " ( ~P s  i^i  Fin )
)  C_  s
1911, 18wb 176 . . . . . . 7  wff  ( s  e.  c  <->  U. (
f " ( ~P s  i^i  Fin )
)  C_  s )
2019, 9, 5wral 2545 . . . . . 6  wff  A. s  e.  ~P  x ( s  e.  c  <->  U. (
f " ( ~P s  i^i  Fin )
)  C_  s )
218, 20wa 358 . . . . 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 1530 . . . 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 13486 . . . . 5  class Moore
244, 23cfv 5257 . . . 4  class  (Moore `  x )
2522, 10, 24crab 2549 . . 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 4079 . 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 1625 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  13555
  Copyright terms: Public domain W3C validator