Theorem mrissmrcd

Description: In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd , and so are equal by mrieqv2d .) (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mrissmrcd.1	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
2		mrissmrcd.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
3		mrissmrcd.3	$$⊢I=\mathrm{mrInd}\left(A\right)$$
4		mrissmrcd.4	$$⊢\phi \to S\subseteq N\left(T\right)$$
5		mrissmrcd.5	$$⊢\phi \to T\subseteq S$$
6		mrissmrcd.6	$$⊢\phi \to S\in I$$
7	1 2 4 5	mressmrcd	$$⊢\phi \to N\left(S\right)=N\left(T\right)$$
8		pssne	$$⊢N\left(T\right)\subset N\left(S\right)\to N\left(T\right)\ne N\left(S\right)$$
9	8	necomd	$$⊢N\left(T\right)\subset N\left(S\right)\to N\left(S\right)\ne N\left(T\right)$$
10	9	necon2bi	$$⊢N\left(S\right)=N\left(T\right)\to \neg N\left(T\right)\subset N\left(S\right)$$
11	7 10	syl	$$⊢\phi \to \neg N\left(T\right)\subset N\left(S\right)$$
12	3 1 6	mrissd	$$⊢\phi \to S\subseteq X$$
13	1 2 3 12	mrieqv2d	$$⊢\phi \to \left(S\in I\leftrightarrow \forall s\left(s\subset S\to N\left(s\right)\subset N\left(S\right)\right)\right)$$
14	6 13	mpbid	$$⊢\phi \to \forall s\left(s\subset S\to N\left(s\right)\subset N\left(S\right)\right)$$
15	6 5	ssexd	$$⊢\phi \to T\in \mathrm{V}$$
16		simpr	$$⊢\left(\phi \wedge s=T\right)\to s=T$$
17	16	psseq1d	$$⊢\left(\phi \wedge s=T\right)\to \left(s\subset S\leftrightarrow T\subset S\right)$$
18	16	fveq2d	$$⊢\left(\phi \wedge s=T\right)\to N\left(s\right)=N\left(T\right)$$
19	18	psseq1d	$$⊢\left(\phi \wedge s=T\right)\to \left(N\left(s\right)\subset N\left(S\right)\leftrightarrow N\left(T\right)\subset N\left(S\right)\right)$$
20	17 19	imbi12d	$$⊢\left(\phi \wedge s=T\right)\to \left(\left(s\subset S\to N\left(s\right)\subset N\left(S\right)\right)\leftrightarrow \left(T\subset S\to N\left(T\right)\subset N\left(S\right)\right)\right)$$
21	15 20	spcdv	$$⊢\phi \to \left(\forall s\left(s\subset S\to N\left(s\right)\subset N\left(S\right)\right)\to \left(T\subset S\to N\left(T\right)\subset N\left(S\right)\right)\right)$$
22	14 21	mpd	$$⊢\phi \to \left(T\subset S\to N\left(T\right)\subset N\left(S\right)\right)$$
23	11 22	mtod	$$⊢\phi \to \neg T\subset S$$
24		sspss	$$⊢T\subseteq S\leftrightarrow \left(T\subset S\vee T=S\right)$$
25	5 24	sylib	$$⊢\phi \to \left(T\subset S\vee T=S\right)$$
26	25	ord	$$⊢\phi \to \left(\neg T\subset S\to T=S\right)$$
27	23 26	mpd	$$⊢\phi \to T=S$$
28	27	eqcomd	$$⊢\phi \to S=T$$