Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-nacs Unicode version

Definition df-nacs 26881
Description: Define a closure system of Noetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
Assertion
Ref Expression
df-nacs  |- NoeACS  =  ( x  e.  _V  |->  { c  e.  (ACS `  x )  |  A. s  e.  c  E. g  e.  ( ~P x  i^i  Fin ) s  =  ( (mrCls `  c ) `  g
) } )
Distinct variable group:    x, c, s, g

Detailed syntax breakdown of Definition df-nacs
StepHypRef Expression
1 cnacs 26880 . 2  class NoeACS
2 vx . . 3  set  x
3 cvv 2801 . . 3  class  _V
4 vs . . . . . . . 8  set  s
54cv 1631 . . . . . . 7  class  s
6 vg . . . . . . . . 9  set  g
76cv 1631 . . . . . . . 8  class  g
8 vc . . . . . . . . . 10  set  c
98cv 1631 . . . . . . . . 9  class  c
10 cmrc 13501 . . . . . . . . 9  class mrCls
119, 10cfv 5271 . . . . . . . 8  class  (mrCls `  c )
127, 11cfv 5271 . . . . . . 7  class  ( (mrCls `  c ) `  g
)
135, 12wceq 1632 . . . . . 6  wff  s  =  ( (mrCls `  c
) `  g )
142cv 1631 . . . . . . . 8  class  x
1514cpw 3638 . . . . . . 7  class  ~P x
16 cfn 6879 . . . . . . 7  class  Fin
1715, 16cin 3164 . . . . . 6  class  ( ~P x  i^i  Fin )
1813, 6, 17wrex 2557 . . . . 5  wff  E. g  e.  ( ~P x  i^i 
Fin ) s  =  ( (mrCls `  c
) `  g )
1918, 4, 9wral 2556 . . . 4  wff  A. s  e.  c  E. g  e.  ( ~P x  i^i 
Fin ) s  =  ( (mrCls `  c
) `  g )
20 cacs 13503 . . . . 5  class ACS
2114, 20cfv 5271 . . . 4  class  (ACS `  x )
2219, 8, 21crab 2560 . . 3  class  { c  e.  (ACS `  x
)  |  A. s  e.  c  E. g  e.  ( ~P x  i^i 
Fin ) s  =  ( (mrCls `  c
) `  g ) }
232, 3, 22cmpt 4093 . 2  class  ( x  e.  _V  |->  { c  e.  (ACS `  x
)  |  A. s  e.  c  E. g  e.  ( ~P x  i^i 
Fin ) s  =  ( (mrCls `  c
) `  g ) } )
241, 23wceq 1632 1  wff NoeACS  =  ( x  e.  _V  |->  { c  e.  (ACS `  x )  |  A. s  e.  c  E. g  e.  ( ~P x  i^i  Fin ) s  =  ( (mrCls `  c ) `  g
) } )
Colors of variables: wff set class
This definition is referenced by:  isnacs  26882
  Copyright terms: Public domain W3C validator