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 | |