This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	\|- ( 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 ) )