Theorem nacsacs

Description: A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015)

	Ref	Expression
Assertion	nacsacs	$$⊢C\in \mathrm{NoeACS}\left(X\right)\to C\in \mathrm{ACS}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{mrCls}\left(C\right)=\mathrm{mrCls}\left(C\right)$$
2	1	isnacs2	$$⊢C\in \mathrm{NoeACS}\left(X\right)\leftrightarrow \left(C\in \mathrm{ACS}\left(X\right)\wedge \mathrm{mrCls}\left(C\right)\left[𝒫X\cap \mathrm{Fin}\right]=C\right)$$
3	2	simplbi	$$⊢C\in \mathrm{NoeACS}\left(X\right)\to C\in \mathrm{ACS}\left(X\right)$$