Theorem mressmrcd

Description: In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mressmrcd.1	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
2		mressmrcd.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
3		mressmrcd.3	$$⊢\phi \to S\subseteq N\left(T\right)$$
4		mressmrcd.4	$$⊢\phi \to T\subseteq S$$
5	1 2	mrcssvd	$$⊢\phi \to N\left(T\right)\subseteq X$$
6	1 2 3 5	mrcssd	$$⊢\phi \to N\left(S\right)\subseteq N\left(N\left(T\right)\right)$$
7	3 5	sstrd	$$⊢\phi \to S\subseteq X$$
8	4 7	sstrd	$$⊢\phi \to T\subseteq X$$
9	1 2 8	mrcidmd	$$⊢\phi \to N\left(N\left(T\right)\right)=N\left(T\right)$$
10	6 9	sseqtrd	$$⊢\phi \to N\left(S\right)\subseteq N\left(T\right)$$
11	1 2 4 7	mrcssd	$$⊢\phi \to N\left(T\right)\subseteq N\left(S\right)$$
12	10 11	eqssd	$$⊢\phi \to N\left(S\right)=N\left(T\right)$$