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 | |- ( ph -> A e. ( ACS ` X ) ) |
|
| acsficld.2 | |- N = ( mrCls ` A ) |
||
| acsficld.3 | |- ( ph -> S C_ X ) |
||
| Assertion | acsficld | |- ( ph -> ( N ` S ) = U. ( N " ( ~P S i^i Fin ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | acsficld.1 | |- ( ph -> A e. ( ACS ` X ) ) |
|
| 2 | acsficld.2 | |- N = ( mrCls ` A ) |
|
| 3 | acsficld.3 | |- ( ph -> S C_ X ) |
|
| 4 | 2 | acsficl | |- ( ( A e. ( ACS ` X ) /\ S C_ X ) -> ( N ` S ) = U. ( N " ( ~P S i^i Fin ) ) ) |
| 5 | 1 3 4 | syl2anc | |- ( ph -> ( N ` S ) = U. ( N " ( ~P S i^i Fin ) ) ) |