Theorem mrcidmd

Description: Moore closure is idempotent. Deduction form of mrcidm . (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mrcssidd.1	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
2		mrcssidd.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
3		mrcssidd.3	$$⊢\phi \to U\subseteq X$$
4	2	mrcidm	$$⊢\left(A\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to N\left(N\left(U\right)\right)=N\left(U\right)$$
5	1 3 4	syl2anc	$$⊢\phi \to N\left(N\left(U\right)\right)=N\left(U\right)$$