Description: An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mriss.1 | |- I = ( mrInd ` A ) |
|
mrissd.2 | |- ( ph -> A e. ( Moore ` X ) ) |
||
mrissd.3 | |- ( ph -> S e. I ) |
||
Assertion | mrissd | |- ( ph -> S C_ X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mriss.1 | |- I = ( mrInd ` A ) |
|
2 | mrissd.2 | |- ( ph -> A e. ( Moore ` X ) ) |
|
3 | mrissd.3 | |- ( ph -> S e. I ) |
|
4 | 1 | mriss | |- ( ( A e. ( Moore ` X ) /\ S e. I ) -> S C_ X ) |
5 | 2 3 4 | syl2anc | |- ( ph -> S C_ X ) |