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

Metamath Proof Explorer

Theorem mrissd

Description: An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mriss.1 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
mrissd.2 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
mrissd.3 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
Assertion mrissd ( 𝜑 → 𝑆 ⊆ 𝑋 )

Proof

Step Hyp Ref Expression
1 mriss.1 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
2 mrissd.2 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
3 mrissd.3 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
4 1 mriss ⊢ ( ( 𝐴 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ⊆ 𝑋 )
5 2 3 4 syl2anc ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )