Theorem ismri2dad

Description: Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	ismri2dad.1	$$⊢N=\mathrm{mrCls}\left(A\right)$$
	ismri2dad.2	$$⊢I=\mathrm{mrInd}\left(A\right)$$
	ismri2dad.3	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
	ismri2dad.4	$$⊢\phi \to S\in I$$
	ismri2dad.5	$$⊢\phi \to Y\in S$$
Assertion	ismri2dad	$$⊢\phi \to \neg Y\in N\left(S\setminus \left\{Y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismri2dad.1	$$⊢N=\mathrm{mrCls}\left(A\right)$$
2		ismri2dad.2	$$⊢I=\mathrm{mrInd}\left(A\right)$$
3		ismri2dad.3	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
4		ismri2dad.4	$$⊢\phi \to S\in I$$
5		ismri2dad.5	$$⊢\phi \to Y\in S$$
6	2 3 4	mrissd	$$⊢\phi \to S\subseteq X$$
7	1 2 3 6	ismri2d	$$⊢\phi \to \left(S\in I\leftrightarrow \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)\right)$$
8	4 7	mpbid	$$⊢\phi \to \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)$$
9		simpr	$$⊢\left(\phi \wedge x=Y\right)\to x=Y$$
10	9	sneqd	$$⊢\left(\phi \wedge x=Y\right)\to \left\{x\right\}=\left\{Y\right\}$$
11	10	difeq2d	$$⊢\left(\phi \wedge x=Y\right)\to S\setminus \left\{x\right\}=S\setminus \left\{Y\right\}$$
12	11	fveq2d	$$⊢\left(\phi \wedge x=Y\right)\to N\left(S\setminus \left\{x\right\}\right)=N\left(S\setminus \left\{Y\right\}\right)$$
13	9 12	eleq12d	$$⊢\left(\phi \wedge x=Y\right)\to \left(x\in N\left(S\setminus \left\{x\right\}\right)\leftrightarrow Y\in N\left(S\setminus \left\{Y\right\}\right)\right)$$
14	13	notbid	$$⊢\left(\phi \wedge x=Y\right)\to \left(\neg x\in N\left(S\setminus \left\{x\right\}\right)\leftrightarrow \neg Y\in N\left(S\setminus \left\{Y\right\}\right)\right)$$
15	5 14	rspcdv	$$⊢\phi \to \left(\forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)\to \neg Y\in N\left(S\setminus \left\{Y\right\}\right)\right)$$
16	8 15	mpd	$$⊢\phi \to \neg Y\in N\left(S\setminus \left\{Y\right\}\right)$$