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

Metamath Proof Explorer

Theorem mriss

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

		Ref	Expression
	Hypothesis	mriss.1	$⊢ I = mrInd (A)$
	Assertion	mriss	$⊢ (A \in Moore (X) \land S \in I) \to S \subseteq X$

Step	Hyp	Ref	Expression
1		mriss.1	$⊢ I = mrInd (A)$
2		eqid	$⊢ mrCls (A) = mrCls (A)$
3	2 1	ismri	$⊢ A \in Moore (X) \to (S \in I \leftrightarrow (S \subseteq X \land \forall x \in S \neg x \in mrCls (A) (S ∖ \{x\})))$
4	3	simprbda	$⊢ (A \in Moore (X) \land S \in I) \to S \subseteq X$