Theorem mriss

Description: An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypothesis	mriss.1	$$⊢I=\mathrm{mrInd}\left(A\right)$$
Assertion	mriss	$$⊢\left(A\in \mathrm{Moore}\left(X\right)\wedge S\in I\right)\to S\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		mriss.1	$$⊢I=\mathrm{mrInd}\left(A\right)$$
2		eqid	$$⊢\mathrm{mrCls}\left(A\right)=\mathrm{mrCls}\left(A\right)$$
3	2 1	ismri	$$⊢A\in \mathrm{Moore}\left(X\right)\to \left(S\in I\leftrightarrow \left(S\subseteq X\wedge \forall x\in S\neg x\in \mathrm{mrCls}\left(A\right)\left(S\setminus \left\{x\right\}\right)\right)\right)$$
4	3	simprbda	$$⊢\left(A\in \mathrm{Moore}\left(X\right)\wedge S\in I\right)\to S\subseteq X$$