Theorem ismri2

Description: Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	ismri2.1	$$⊢N=\mathrm{mrCls}\left(A\right)$$
	ismri2.2	$$⊢I=\mathrm{mrInd}\left(A\right)$$
Assertion	ismri2	$$⊢\left(A\in \mathrm{Moore}\left(X\right)\wedge S\subseteq X\right)\to \left(S\in I\leftrightarrow \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismri2.1	$$⊢N=\mathrm{mrCls}\left(A\right)$$
2		ismri2.2	$$⊢I=\mathrm{mrInd}\left(A\right)$$
3	1 2	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 N\left(S\setminus \left\{x\right\}\right)\right)\right)$$
4	3	baibd	$$⊢\left(A\in \mathrm{Moore}\left(X\right)\wedge S\subseteq X\right)\to \left(S\in I\leftrightarrow \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)\right)$$