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 ⊢ I = mrInd ⁡ A
mrissd.2 ⊢ φ → A ∈ Moore ⁡ X
mrissd.3 ⊢ φ → S ∈ I
Assertion mrissd ⊢ φ → S ⊆ X

Proof

Step Hyp Ref Expression
1 mriss.1 ⊢ I = mrInd ⁡ A
2 mrissd.2 ⊢ φ → A ∈ Moore ⁡ X
3 mrissd.3 ⊢ φ → S ∈ I
4 1 mriss ⊢ A ∈ Moore ⁡ X ∧ S ∈ I → S ⊆ X
5 2 3 4 syl2anc ⊢ φ → S ⊆ X