Definition df-nacs 40228

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 = (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})

Distinct variable group:   𝑥,𝑐,𝑠,𝑔

Detailed syntax breakdown of Definition df-nacs

Step	Hyp	Ref	Expression
1		cnacs 40227	. 2 class NoeACS
2		vx	. . 3 setvar 𝑥
3		cvv 3408	. . 3 class V
4		vs	. . . . . . . 8 setvar 𝑠
5	4	cv 1542	. . . . . . 7 class 𝑠
6		vg	. . . . . . . . 9 setvar 𝑔
7	6	cv 1542	. . . . . . . 8 class 𝑔
8		vc	. . . . . . . . . 10 setvar 𝑐
9	8	cv 1542	. . . . . . . . 9 class 𝑐
10		cmrc 17086	. . . . . . . . 9 class mrCls
11	9, 10	cfv 6380	. . . . . . . 8 class (mrCls‘𝑐)
12	7, 11	cfv 6380	. . . . . . 7 class ((mrCls‘𝑐)‘𝑔)
13	5, 12	wceq 1543	. . . . . 6 wff 𝑠 = ((mrCls‘𝑐)‘𝑔)
14	2	cv 1542	. . . . . . . 8 class 𝑥
15	14	cpw 4513	. . . . . . 7 class 𝒫 𝑥
16		cfn 8626	. . . . . . 7 class Fin
17	15, 16	cin 3865	. . . . . 6 class (𝒫 𝑥 ∩ Fin)
18	13, 6, 17	wrex 3062	. . . . 5 wff ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)
19	18, 4, 9	wral 3061	. . . 4 wff ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)
20		cacs 17088	. . . . 5 class ACS
21	14, 20	cfv 6380	. . . 4 class (ACS‘𝑥)
22	19, 8, 21	crab 3065	. . 3 class {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)}
23	2, 3, 22	cmpt 5135	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})
24	1, 23	wceq 1543	1 wff NoeACS = (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})

This definition is referenced by:  isnacs  40229