Theorem ismri2dd

Description: Definition of independence of a subset of the base set in a Moore system. One-way 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$$
	ismri2dd.5	$$⊢\phi \to \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)$$
Assertion	ismri2dd	$$⊢\phi \to S\in I$$

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		ismri2dd.5	$$⊢\phi \to \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)$$
6	1 2 3 4	ismri2d	$$⊢\phi \to \left(S\in I\leftrightarrow \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)\right)$$
7	5 6	mpbird	$$⊢\phi \to S\in I$$