Metamath Proof Explorer


Theorem mrissd

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 )

Proof

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 )