Theorem acsfiel2

Description: A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Hypothesis	isacs2.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
Assertion	acsfiel2	$$⊢\left(C\in \mathrm{ACS}\left(X\right)\wedge S\subseteq X\right)\to \left(S\in C\leftrightarrow \forall y\in \left(𝒫S\cap \mathrm{Fin}\right)F\left(y\right)\subseteq S\right)$$

Proof

Step	Hyp	Ref	Expression
1		isacs2.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
2	1	acsfiel	$$⊢C\in \mathrm{ACS}\left(X\right)\to \left(S\in C\leftrightarrow \left(S\subseteq X\wedge \forall y\in \left(𝒫S\cap \mathrm{Fin}\right)F\left(y\right)\subseteq S\right)\right)$$
3	2	baibd	$$⊢\left(C\in \mathrm{ACS}\left(X\right)\wedge S\subseteq X\right)\to \left(S\in C\leftrightarrow \forall y\in \left(𝒫S\cap \mathrm{Fin}\right)F\left(y\right)\subseteq S\right)$$