Description: A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | nacsacs | ⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( mrCls ‘ 𝐶 ) = ( mrCls ‘ 𝐶 ) | |
2 | 1 | isnacs2 | ⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ( ( mrCls ‘ 𝐶 ) “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) ) |
3 | 2 | simplbi | ⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) ) |