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

Metamath Proof Explorer

Theorem mrcssidd

Description: A set is contained in its Moore closure. Deduction form of mrcssid . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrcssidd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
mrcssidd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
mrcssidd.3 ⊢ ( 𝜑 → 𝑈 ⊆ 𝑋 )
Assertion mrcssidd ( 𝜑 → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 mrcssidd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mrcssidd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 mrcssidd.3 ⊢ ( 𝜑 → 𝑈 ⊆ 𝑋 )
4 2 mrcssid ⊢ ( ( 𝐴 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )
5 1 3 4 syl2anc ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )