Description: Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismri2.1 | |- N = ( mrCls ` A ) |
|
ismri2.2 | |- I = ( mrInd ` A ) |
||
ismri2d.3 | |- ( ph -> A e. ( Moore ` X ) ) |
||
ismri2d.4 | |- ( ph -> S C_ X ) |
||
ismri2dd.5 | |- ( ph -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) |
||
Assertion | ismri2dd | |- ( ph -> S e. I ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismri2.1 | |- N = ( mrCls ` A ) |
|
2 | ismri2.2 | |- I = ( mrInd ` A ) |
|
3 | ismri2d.3 | |- ( ph -> A e. ( Moore ` X ) ) |
|
4 | ismri2d.4 | |- ( ph -> S C_ X ) |
|
5 | ismri2dd.5 | |- ( ph -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) |
|
6 | 1 2 3 4 | ismri2d | |- ( ph -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) |
7 | 5 6 | mpbird | |- ( ph -> S e. I ) |