Description: A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | isacs2.f | |- F = ( mrCls ` C ) |
|
| Assertion | acsfiel2 | |- ( ( C e. ( ACS ` X ) /\ S C_ X ) -> ( S e. C <-> A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isacs2.f | |- F = ( mrCls ` C ) |
|
| 2 | 1 | acsfiel | |- ( C e. ( ACS ` X ) -> ( S e. C <-> ( S C_ X /\ A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) ) ) |
| 3 | 2 | baibd | |- ( ( C e. ( ACS ` X ) /\ S C_ X ) -> ( S e. C <-> A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) ) |