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	|- ( ph -> A e. ( Moore ` X ) )
	mressmrcd.2	|- N = ( mrCls ` A )
	mressmrcd.3	|- ( ph -> S C_ ( N ` T ) )
	mressmrcd.4	|- ( ph -> T C_ S )
Assertion	mressmrcd	|- ( ph -> ( N ` S ) = ( N ` T ) )

Proof

Step	Hyp	Ref	Expression
1		mressmrcd.1	|- ( ph -> A e. ( Moore ` X ) )
2		mressmrcd.2	|- N = ( mrCls ` A )
3		mressmrcd.3	|- ( ph -> S C_ ( N ` T ) )
4		mressmrcd.4	|- ( ph -> T C_ S )
5	1 2	mrcssvd	|- ( ph -> ( N ` T ) C_ X )
6	1 2 3 5	mrcssd	|- ( ph -> ( N ` S ) C_ ( N ` ( N ` T ) ) )
7	3 5	sstrd	|- ( ph -> S C_ X )
8	4 7	sstrd	|- ( ph -> T C_ X )
9	1 2 8	mrcidmd	|- ( ph -> ( N ` ( N ` T ) ) = ( N ` T ) )
10	6 9	sseqtrd	|- ( ph -> ( N ` S ) C_ ( N ` T ) )
11	1 2 4 7	mrcssd	|- ( ph -> ( N ` T ) C_ ( N ` S ) )
12	10 11	eqssd	|- ( ph -> ( N ` S ) = ( N ` T ) )