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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnacs	⊢ NoeACS
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vc	⊢ 𝑐
4		cacs	⊢ ACS
5	1	cv	⊢ 𝑥
6	5 4	cfv	⊢ ( ACS ‘ 𝑥 )
7		vs	⊢ 𝑠
8	3	cv	⊢ 𝑐
9		vg	⊢ 𝑔
10	5	cpw	⊢ 𝒫 𝑥
11		cfn	⊢ Fin
12	10 11	cin	⊢ ( 𝒫 𝑥 ∩ Fin )
13	7	cv	⊢ 𝑠
14		cmrc	⊢ mrCls
15	8 14	cfv	⊢ ( mrCls ‘ 𝑐 )
16	9	cv	⊢ 𝑔
17	16 15	cfv	⊢ ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 )
18	13 17	wceq	⊢ 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 )
19	18 9 12	wrex	⊢ ∃ 𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 )
20	19 7 8	wral	⊢ ∀ 𝑠 ∈ 𝑐 ∃ 𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 )
21	20 3 6	crab	⊢ { 𝑐 ∈ ( ACS ‘ 𝑥 ) ∣ ∀ 𝑠 ∈ 𝑐 ∃ 𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) }
22	1 2 21	cmpt	⊢ ( 𝑥 ∈ V ↦ { 𝑐 ∈ ( ACS ‘ 𝑥 ) ∣ ∀ 𝑠 ∈ 𝑐 ∃ 𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } )
23	0 22	wceq	⊢ NoeACS = ( 𝑥 ∈ V ↦ { 𝑐 ∈ ( ACS ‘ 𝑥 ) ∣ ∀ 𝑠 ∈ 𝑐 ∃ 𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } )