Theorem mrcssd

Description: Moore closure preserves subset ordering. Deduction form of mrcss . (Contributed by David Moews, 1-May-2017)

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

Proof

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