Metamath Proof Explorer

Definition df-nacs

Description: Define a closure system ofNoetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Assertion 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 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnacs 
 |-  NoeACS
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vc 
 |-  c
4 cacs 
 |-  ACS
5 1 cv 
 |-  x
6 5 4 cfv 
 |-  ( ACS ` x )
7 vs 
 |-  s
8 3 cv 
 |-  c
9 vg 
 |-  g
10 5 cpw 
 |-  ~P x
11 cfn 
 |-  Fin
12 10 11 cin 
 |-  ( ~P x i^i Fin )
13 7 cv 
 |-  s
14 cmrc 
 |-  mrCls
15 8 14 cfv 
 |-  ( mrCls ` c )
16 9 cv 
 |-  g
17 16 15 cfv 
 |-  ( ( mrCls ` c ) ` g )
18 13 17 wceq 
 |-  s = ( ( mrCls ` c ) ` g )
19 18 9 12 wrex 
 |-  E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g )
20 19 7 8 wral 
 |-  A. s e. c E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g )
21 20 3 6 crab 
 |-  { c e. ( ACS ` x ) | A. s e. c E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g ) }
22 1 2 21 cmpt 
 |-  ( x e. _V |-> { c e. ( ACS ` x ) | A. s e. c E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g ) } )
23 0 22 wceq 
 |-  NoeACS = ( x e. _V |-> { c e. ( ACS ` x ) | A. s e. c E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g ) } )