Metamath Proof Explorer


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 φAACSX
acsficld.2 N=mrClsA
acsficld.3 φSX
Assertion acsficld φNS=N𝒫SFin

Proof

Step Hyp Ref Expression
1 acsficld.1 φAACSX
2 acsficld.2 N=mrClsA
3 acsficld.3 φSX
4 2 acsficl AACSXSXNS=N𝒫SFin
5 1 3 4 syl2anc φNS=N𝒫SFin