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 ⊢ ( 𝜑 → 𝐴 ∈ ( 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 ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )