Theorem mrissmrid

Description: In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mrissmrid.1	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
2		mrissmrid.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
3		mrissmrid.3	$$⊢I=\mathrm{mrInd}\left(A\right)$$
4		mrissmrid.4	$$⊢\phi \to S\in I$$
5		mrissmrid.5	$$⊢\phi \to T\subseteq S$$
6	3 1 4	mrissd	$$⊢\phi \to S\subseteq X$$
7	5 6	sstrd	$$⊢\phi \to T\subseteq X$$
8	2 3 1 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)$$
9	4 8	mpbid	$$⊢\phi \to \forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)$$
10	5	sseld	$$⊢\phi \to \left(x\in T\to x\in S\right)$$
11	5	ssdifd	$$⊢\phi \to T\setminus \left\{x\right\}\subseteq S\setminus \left\{x\right\}$$
12	6	ssdifssd	$$⊢\phi \to S\setminus \left\{x\right\}\subseteq X$$
13	1 2 11 12	mrcssd	$$⊢\phi \to N\left(T\setminus \left\{x\right\}\right)\subseteq N\left(S\setminus \left\{x\right\}\right)$$
14	13	ssneld	$$⊢\phi \to \left(\neg x\in N\left(S\setminus \left\{x\right\}\right)\to \neg x\in N\left(T\setminus \left\{x\right\}\right)\right)$$
15	10 14	imim12d	$$⊢\phi \to \left(\left(x\in S\to \neg x\in N\left(S\setminus \left\{x\right\}\right)\right)\to \left(x\in T\to \neg x\in N\left(T\setminus \left\{x\right\}\right)\right)\right)$$
16	15	ralimdv2	$$⊢\phi \to \left(\forall x\in S\neg x\in N\left(S\setminus \left\{x\right\}\right)\to \forall x\in T\neg x\in N\left(T\setminus \left\{x\right\}\right)\right)$$
17	9 16	mpd	$$⊢\phi \to \forall x\in T\neg x\in N\left(T\setminus \left\{x\right\}\right)$$
18	2 3 1 7 17	ismri2dd	$$⊢\phi \to T\in I$$