# Metamath Proof Explorer

## Theorem acsfiel

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

Ref Expression
Hypothesis isacs2.f ${⊢}{F}=\mathrm{mrCls}\left({C}\right)$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 isacs2.f ${⊢}{F}=\mathrm{mrCls}\left({C}\right)$
2 acsmre ${⊢}{C}\in \mathrm{ACS}\left({X}\right)\to {C}\in \mathrm{Moore}\left({X}\right)$
3 mress ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {S}\in {C}\right)\to {S}\subseteq {X}$
4 2 3 sylan ${⊢}\left({C}\in \mathrm{ACS}\left({X}\right)\wedge {S}\in {C}\right)\to {S}\subseteq {X}$
5 4 ex ${⊢}{C}\in \mathrm{ACS}\left({X}\right)\to \left({S}\in {C}\to {S}\subseteq {X}\right)$
6 5 pm4.71rd ${⊢}{C}\in \mathrm{ACS}\left({X}\right)\to \left({S}\in {C}↔\left({S}\subseteq {X}\wedge {S}\in {C}\right)\right)$
7 eleq1 ${⊢}{s}={S}\to \left({s}\in {C}↔{S}\in {C}\right)$
8 pweq ${⊢}{s}={S}\to 𝒫{s}=𝒫{S}$
9 8 ineq1d ${⊢}{s}={S}\to 𝒫{s}\cap \mathrm{Fin}=𝒫{S}\cap \mathrm{Fin}$
10 sseq2 ${⊢}{s}={S}\to \left({F}\left({y}\right)\subseteq {s}↔{F}\left({y}\right)\subseteq {S}\right)$
11 9 10 raleqbidv ${⊢}{s}={S}\to \left(\forall {y}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\subseteq {s}↔\forall {y}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\subseteq {S}\right)$
12 7 11 bibi12d ${⊢}{s}={S}\to \left(\left({s}\in {C}↔\forall {y}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\subseteq {s}\right)↔\left({S}\in {C}↔\forall {y}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\subseteq {S}\right)\right)$
13 1 isacs2 ${⊢}{C}\in \mathrm{ACS}\left({X}\right)↔\left({C}\in \mathrm{Moore}\left({X}\right)\wedge \forall {s}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({s}\in {C}↔\forall {y}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\subseteq {s}\right)\right)$
14 13 simprbi ${⊢}{C}\in \mathrm{ACS}\left({X}\right)\to \forall {s}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({s}\in {C}↔\forall {y}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\subseteq {s}\right)$
15 14 adantr ${⊢}\left({C}\in \mathrm{ACS}\left({X}\right)\wedge {S}\subseteq {X}\right)\to \forall {s}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({s}\in {C}↔\forall {y}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\subseteq {s}\right)$
16 elfvdm ${⊢}{C}\in \mathrm{ACS}\left({X}\right)\to {X}\in \mathrm{dom}\mathrm{ACS}$
17 elpw2g ${⊢}{X}\in \mathrm{dom}\mathrm{ACS}\to \left({S}\in 𝒫{X}↔{S}\subseteq {X}\right)$
18 16 17 syl ${⊢}{C}\in \mathrm{ACS}\left({X}\right)\to \left({S}\in 𝒫{X}↔{S}\subseteq {X}\right)$
19 18 biimpar ${⊢}\left({C}\in \mathrm{ACS}\left({X}\right)\wedge {S}\subseteq {X}\right)\to {S}\in 𝒫{X}$
20 12 15 19 rspcdva ${⊢}\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)$
21 20 pm5.32da ${⊢}{C}\in \mathrm{ACS}\left({X}\right)\to \left(\left({S}\subseteq {X}\wedge {S}\in {C}\right)↔\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)$
22 6 21 bitrd ${⊢}{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)$