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 | ||
acsficld.2 | |||
acsficld.3 | |||
Assertion | acsficld |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | acsficld.1 | ||
2 | acsficld.2 | ||
3 | acsficld.3 | ||
4 | 2 | acsficl | |
5 | 1 3 4 | syl2anc |