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 ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 eqid ( mrCls ‘ 𝐶 ) = ( mrCls ‘ 𝐶 )
2 1 isnacs2 ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ( ( mrCls ‘ 𝐶 ) “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) )
3 2 simplbi ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) )