Metamath Proof Explorer

Theorem acsmre

Description: Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion acsmre 
|- ( C e. ( ACS ` X ) -> C e. ( Moore ` X ) )

Proof

Step Hyp Ref Expression
1 isacs 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) )
2 1 simplbi 
 |-  ( C e. ( ACS ` X ) -> C e. ( Moore ` X ) )