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

Metamath Proof Explorer

Theorem ismri2dd

Description: Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	ismri2.1	$⊢ N = mrCls (A)$
	ismri2.2	$⊢ I = mrInd (A)$
	ismri2d.3	$⊢ φ \to A \in Moore (X)$
	ismri2d.4	$⊢ φ \to S \subseteq X$
	ismri2dd.5	$⊢ φ \to \forall x \in S \neg x \in N (S ∖ \{x\})$
Assertion	ismri2dd	$⊢ φ \to S \in I$

Proof

Step	Hyp	Ref	Expression
1		ismri2.1	$⊢ N = mrCls (A)$
2		ismri2.2	$⊢ I = mrInd (A)$
3		ismri2d.3	$⊢ φ \to A \in Moore (X)$
4		ismri2d.4	$⊢ φ \to S \subseteq X$
5		ismri2dd.5	$⊢ φ \to \forall x \in S \neg x \in N (S ∖ \{x\})$
6	1 2 3 4	ismri2d	$⊢ φ \to (S \in I \leftrightarrow \forall x \in S \neg x \in N (S ∖ \{x\}))$
7	5 6	mpbird	$⊢ φ \to S \in I$