Theorem mrieqvlemd

Description: In a Moore system, if Y is a member of S , ( S \ { Y } ) and S have the same closure if and only if Y is in the closure of ( S \ { Y } ) . Used in the proof of mrieqvd and mrieqv2d . Deduction form. (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mrieqvlemd.1	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
2		mrieqvlemd.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
3		mrieqvlemd.3	$$⊢\phi \to S\subseteq X$$
4		mrieqvlemd.4	$$⊢\phi \to Y\in S$$
5	1	adantr	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to A\in \mathrm{Moore}\left(X\right)$$
6		undif1	$$⊢\left(S\setminus \left\{Y\right\}\right)\cup \left\{Y\right\}=S\cup \left\{Y\right\}$$
7	3	adantr	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to S\subseteq X$$
8	7	ssdifssd	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to S\setminus \left\{Y\right\}\subseteq X$$
9	5 2 8	mrcssidd	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to S\setminus \left\{Y\right\}\subseteq N\left(S\setminus \left\{Y\right\}\right)$$
10		simpr	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to Y\in N\left(S\setminus \left\{Y\right\}\right)$$
11	10	snssd	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to \left\{Y\right\}\subseteq N\left(S\setminus \left\{Y\right\}\right)$$
12	9 11	unssd	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to \left(S\setminus \left\{Y\right\}\right)\cup \left\{Y\right\}\subseteq N\left(S\setminus \left\{Y\right\}\right)$$
13	6 12	eqsstrrid	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to S\cup \left\{Y\right\}\subseteq N\left(S\setminus \left\{Y\right\}\right)$$
14	13	unssad	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to S\subseteq N\left(S\setminus \left\{Y\right\}\right)$$
15		difssd	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to S\setminus \left\{Y\right\}\subseteq S$$
16	5 2 14 15	mressmrcd	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to N\left(S\right)=N\left(S\setminus \left\{Y\right\}\right)$$
17	16	eqcomd	$$⊢\left(\phi \wedge Y\in N\left(S\setminus \left\{Y\right\}\right)\right)\to N\left(S\setminus \left\{Y\right\}\right)=N\left(S\right)$$
18	1 2 3	mrcssidd	$$⊢\phi \to S\subseteq N\left(S\right)$$
19	18 4	sseldd	$$⊢\phi \to Y\in N\left(S\right)$$
20	19	adantr	$$⊢\left(\phi \wedge N\left(S\setminus \left\{Y\right\}\right)=N\left(S\right)\right)\to Y\in N\left(S\right)$$
21		simpr	$$⊢\left(\phi \wedge N\left(S\setminus \left\{Y\right\}\right)=N\left(S\right)\right)\to N\left(S\setminus \left\{Y\right\}\right)=N\left(S\right)$$
22	20 21	eleqtrrd	$$⊢\left(\phi \wedge N\left(S\setminus \left\{Y\right\}\right)=N\left(S\right)\right)\to Y\in N\left(S\setminus \left\{Y\right\}\right)$$
23	17 22	impbida	$$⊢\phi \to \left(Y\in N\left(S\setminus \left\{Y\right\}\right)\leftrightarrow N\left(S\setminus \left\{Y\right\}\right)=N\left(S\right)\right)$$