Theorem ismri2d

Description: Criterion for a subset of the base set in a Moore system to be independent. Deduction form. (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)$$
	ismri2d.3	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
	ismri2d.4	$$⊢\phi \to S\subseteq X$$
Assertion	ismri2d	$$⊢\phi \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		ismri2d.3	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
4		ismri2d.4	$$⊢\phi \to S\subseteq X$$
5	1 2	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)$$
6	3 4 5	syl2anc	$$⊢\phi \to \left(S\in I\leftrightarrow \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)\right)$$