Metamath Proof Explorer

Theorem nacsacs

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

Ref Expression
Assertion nacsacs ⊢ C ∈ NoeACS ⁡ X → C ∈ ACS ⁡ X

Proof

Step Hyp Ref Expression
1 eqid ⊢ mrCls ⁡ C = mrCls ⁡ C
2 1 isnacs2 ⊢ C ∈ NoeACS ⁡ X ↔ C ∈ ACS ⁡ X ∧ mrCls ⁡ C 𝒫 X ∩ Fin = C
3 2 simplbi ⊢ C ∈ NoeACS ⁡ X → C ∈ ACS ⁡ X