Metamath Proof Explorer


Theorem mrcssd

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

Ref Expression
Hypotheses mrcssd.1 φAMooreX
mrcssd.2 N=mrClsA
mrcssd.3 φUV
mrcssd.4 φVX
Assertion mrcssd φNUNV

Proof

Step Hyp Ref Expression
1 mrcssd.1 φAMooreX
2 mrcssd.2 N=mrClsA
3 mrcssd.3 φUV
4 mrcssd.4 φVX
5 2 mrcss AMooreXUVVXNUNV
6 1 3 4 5 syl3anc φNUNV