Theorem mrcssidd

Description: A set is contained in its Moore closure. Deduction form of mrcssid . (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	mrcssidd	$$⊢\phi \to U\subseteq 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	mrcssid	$$⊢\left(A\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to U\subseteq N\left(U\right)$$
5	1 3 4	syl2anc	$$⊢\phi \to U\subseteq N\left(U\right)$$