Metamath Proof Explorer


Theorem mressmrcd

Description: In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mressmrcd.1 φAMooreX
mressmrcd.2 N=mrClsA
mressmrcd.3 φSNT
mressmrcd.4 φTS
Assertion mressmrcd φNS=NT

Proof

Step Hyp Ref Expression
1 mressmrcd.1 φAMooreX
2 mressmrcd.2 N=mrClsA
3 mressmrcd.3 φSNT
4 mressmrcd.4 φTS
5 1 2 mrcssvd φNTX
6 1 2 3 5 mrcssd φNSNNT
7 3 5 sstrd φSX
8 4 7 sstrd φTX
9 1 2 8 mrcidmd φNNT=NT
10 6 9 sseqtrd φNSNT
11 1 2 4 7 mrcssd φNTNS
12 10 11 eqssd φNS=NT