Definition df-nacs 37266

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

Step	Hyp	Ref	Expression
1		cnacs 37265	. 2 class NoeACS
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vs	. . . . . . . 8 setvar s
5	4	cv 1482	. . . . . . 7 class s
6		vg	. . . . . . . . 9 setvar g
7	6	cv 1482	. . . . . . . 8 class g
8		vc	. . . . . . . . . 10 setvar c
9	8	cv 1482	. . . . . . . . 9 class c
10		cmrc 16243	. . . . . . . . 9 class mrCls
11	9, 10	cfv 5888	. . . . . . . 8 class (mrCls ` c )
12	7, 11	cfv 5888	. . . . . . 7 class ( (mrCls ` c ) ` g )
13	5, 12	wceq 1483	. . . . . 6 wff s = ( (mrCls ` c ) ` g )
14	2	cv 1482	. . . . . . . 8 class x
15	14	cpw 4158	. . . . . . 7 class ~P x
16		cfn 7955	. . . . . . 7 class Fin
17	15, 16	cin 3573	. . . . . 6 class ( ~P x i^i Fin )
18	13, 6, 17	wrex 2913	. . . . 5 wff E. g e. ( ~P x i^i Fin ) s = ( (mrCls ` c ) ` g )
19	18, 4, 9	wral 2912	. . . 4 wff A. s e. c E. g e. ( ~P x i^i Fin ) s = ( (mrCls ` c ) ` g )
20		cacs 16245	. . . . 5 class ACS
21	14, 20	cfv 5888	. . . 4 class (ACS ` x )
22	19, 8, 21	crab 2916	. . 3 class { c e. (ACS ` x ) | A. s e. c E. g e. ( ~P x i^i Fin ) s = ( (mrCls ` c ) ` g ) }
23	2, 3, 22	cmpt 4729	. 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 ) } )
24	1, 23	wceq 1483	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 ) } )

This definition is referenced by:  isnacs  37267