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 ∈ V ⟼ c ∈ ACS ⁡ x | ∀ s ∈ c ∃ g ∈ 𝒫 x ∩ 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 ∩ 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 ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g
20 19 7 8 wral wff ∀ s ∈ c ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g
21 20 3 6 crab class c ∈ ACS ⁡ x | ∀ s ∈ c ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g
22 1 2 21 cmpt class x ∈ V ⟼ c ∈ ACS ⁡ x | ∀ s ∈ c ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g
23 0 22 wceq wff NoeACS = x ∈ V ⟼ c ∈ ACS ⁡ x | ∀ s ∈ c ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g