Theorem acsficld

Description: In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	acsficld.1	$$⊢\phi \to A\in \mathrm{ACS}\left(X\right)$$
	acsficld.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
	acsficld.3	$$⊢\phi \to S\subseteq X$$
Assertion	acsficld	$$⊢\phi \to N\left(S\right)=\bigcup N\left[𝒫S\cap \mathrm{Fin}\right]$$

Proof

Step	Hyp	Ref	Expression
1		acsficld.1	$$⊢\phi \to A\in \mathrm{ACS}\left(X\right)$$
2		acsficld.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
3		acsficld.3	$$⊢\phi \to S\subseteq X$$
4	2	acsficl	$$⊢\left(A\in \mathrm{ACS}\left(X\right)\wedge S\subseteq X\right)\to N\left(S\right)=\bigcup N\left[𝒫S\cap \mathrm{Fin}\right]$$
5	1 3 4	syl2anc	$$⊢\phi \to N\left(S\right)=\bigcup N\left[𝒫S\cap \mathrm{Fin}\right]$$