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 ACS X C Moore X

Proof

Step Hyp Ref Expression
1 isacs C ACS X C Moore X f f : 𝒫 X 𝒫 X s 𝒫 X s C f 𝒫 s Fin s
2 1 simplbi C ACS X C Moore X