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 \in V ⟼ \{c \in ACS (x) \| \forall s \in c \exists g \in (𝒫 x \cap Fin) s = mrCls (c) (g)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnacs	$class NoeACS$
1		vx	$setvar x$
2		cvv	$class V$
3		vc	$setvar c$
4		cacs	$class ACS$
5	1	cv	$setvar x$
6	5 4	cfv	$class ACS (x)$
7		vs	$setvar s$
8	3	cv	$setvar c$
9		vg	$setvar g$
10	5	cpw	$class 𝒫 x$
11		cfn	$class Fin$
12	10 11	cin	$class (𝒫 x \cap Fin)$
13	7	cv	$setvar s$
14		cmrc	$class mrCls$
15	8 14	cfv	$class mrCls (c)$
16	9	cv	$setvar g$
17	16 15	cfv	$class mrCls (c) (g)$
18	13 17	wceq	$wff s = mrCls (c) (g)$
19	18 9 12	wrex	$wff \exists g \in (𝒫 x \cap Fin) s = mrCls (c) (g)$
20	19 7 8	wral	$wff \forall s \in c \exists g \in (𝒫 x \cap Fin) s = mrCls (c) (g)$
21	20 3 6	crab	$class \{c \in ACS (x) \| \forall s \in c \exists g \in (𝒫 x \cap Fin) s = mrCls (c) (g)\}$
22	1 2 21	cmpt	$class (x \in V ⟼ \{c \in ACS (x) \| \forall s \in c \exists g \in (𝒫 x \cap Fin) s = mrCls (c) (g)\})$
23	0 22	wceq	$wff NoeACS = (x \in V ⟼ \{c \in ACS (x) \| \forall s \in c \exists g \in (𝒫 x \cap Fin) s = mrCls (c) (g)\})$

Metamath Proof Explorer

Definition df-nacs

Detailed syntax breakdown