Metamath Proof Explorer


Theorem mrcssd

Description: Moore closure preserves subset ordering. Deduction form of mrcss . (Contributed by David Moews, 1-May-2017)

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

Proof

Step Hyp Ref Expression
1 mrcssd.1 ( 𝜑𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mrcssd.2 𝑁 = ( mrCls ‘ 𝐴 )
3 mrcssd.3 ( 𝜑𝑈𝑉 )
4 mrcssd.4 ( 𝜑𝑉𝑋 )
5 2 mrcss ( ( 𝐴 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝑉𝑉𝑋 ) → ( 𝑁𝑈 ) ⊆ ( 𝑁𝑉 ) )
6 1 3 4 5 syl3anc ( 𝜑 → ( 𝑁𝑈 ) ⊆ ( 𝑁𝑉 ) )