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

Metamath Proof Explorer

Theorem ismri2

Description: Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	ismri2.1	$⊢ N = mrCls (A)$
	ismri2.2	$⊢ I = mrInd (A)$
Assertion	ismri2	$⊢ (A \in Moore (X) \land S \subseteq X) \to (S \in I \leftrightarrow \forall x \in S \neg x \in N (S ∖ \{x\}))$

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