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 )