Theorem acsmre

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

	Ref	Expression
Assertion	acsmre	$$⊢C\in \mathrm{ACS}\left(X\right)\to C\in \mathrm{Moore}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		isacs	$$⊢C\in \mathrm{ACS}\left(X\right)\leftrightarrow \left(C\in \mathrm{Moore}\left(X\right)\wedge \exists f\left(f:𝒫X⟶𝒫X\wedge \forall s\in 𝒫X\left(s\in C\leftrightarrow \bigcup f\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right)\right)\right)$$
2	1	simplbi	$$⊢C\in \mathrm{ACS}\left(X\right)\to C\in \mathrm{Moore}\left(X\right)$$