Theorem mrcssd

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

	Ref	Expression
Hypotheses	mrcssd.1	|- ( ph -> A e. ( Moore ` X ) )
	mrcssd.2	|- N = ( mrCls ` A )
	mrcssd.3	|- ( ph -> U C_ V )
	mrcssd.4	|- ( ph -> V C_ X )
Assertion	mrcssd	|- ( ph -> ( N ` U ) C_ ( N ` V ) )

Proof

Step	Hyp	Ref	Expression
1		mrcssd.1	|- ( ph -> A e. ( Moore ` X ) )
2		mrcssd.2	|- N = ( mrCls ` A )
3		mrcssd.3	|- ( ph -> U C_ V )
4		mrcssd.4	|- ( ph -> V C_ X )
5	2	mrcss	|- ( ( A e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> ( N ` U ) C_ ( N ` V ) )
6	1 3 4 5	syl3anc	|- ( ph -> ( N ` U ) C_ ( N ` V ) )