Description: Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismri2.1 | |- N = ( mrCls ` A ) |
|
ismri2.2 | |- I = ( mrInd ` A ) |
||
Assertion | ismri2 | |- ( ( A e. ( Moore ` X ) /\ S C_ X ) -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismri2.1 | |- N = ( mrCls ` A ) |
|
2 | ismri2.2 | |- I = ( mrInd ` A ) |
|
3 | 1 2 | ismri | |- ( A e. ( Moore ` X ) -> ( S e. I <-> ( S C_ X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) ) |
4 | 3 | baibd | |- ( ( A e. ( Moore ` X ) /\ S C_ X ) -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) |