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	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
	mressmrcd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	mressmrcd.3	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑇 ) )
	mressmrcd.4	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
Assertion	mressmrcd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		mressmrcd.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2		mressmrcd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		mressmrcd.3	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑇 ) )
4		mressmrcd.4	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
5	1 2	mrcssvd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑇 ) ⊆ 𝑋 )
6	1 2 3 5	mrcssd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) ⊆ ( 𝑁 ‘ ( 𝑁 ‘ 𝑇 ) ) )
7	3 5	sstrd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
8	4 7	sstrd	⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
9	1 2 8	mrcidmd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑇 ) ) = ( 𝑁 ‘ 𝑇 ) )
10	6 9	sseqtrd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) ⊆ ( 𝑁 ‘ 𝑇 ) )
11	1 2 4 7	mrcssd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑇 ) ⊆ ( 𝑁 ‘ 𝑆 ) )
12	10 11	eqssd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )