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=\mathrm{mrInd}\left(A\right)$$
	mrissd.2	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
	mrissd.3	$$⊢\phi \to S\in I$$
Assertion	mrissd	$$⊢\phi \to S\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		mriss.1	$$⊢I=\mathrm{mrInd}\left(A\right)$$
2		mrissd.2	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
3		mrissd.3	$$⊢\phi \to S\in I$$
4	1	mriss	$$⊢\left(A\in \mathrm{Moore}\left(X\right)\wedge S\in I\right)\to S\subseteq X$$
5	2 3 4	syl2anc	$$⊢\phi \to S\subseteq X$$