# Metamath Proof Explorer

## 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}↔\forall {y}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{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}↔\left({S}\subseteq {X}\wedge \forall {y}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{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}↔\forall {y}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\subseteq {S}\right)$