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 e. ( NoeACS ` X ) -> C e. ( ACS ` X ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( mrCls ` C ) = ( mrCls ` C )
2 1 isnacs2 
 |-  ( C e. ( NoeACS ` X ) <-> ( C e. ( ACS ` X ) /\ ( ( mrCls ` C ) " ( ~P X i^i Fin ) ) = C ) )
3 2 simplbi 
 |-  ( C e. ( NoeACS ` X ) -> C e. ( ACS ` X ) )