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	|- ( ph -> A e. ( Moore ` X ) )
	ismri2d.4	|- ( ph -> S C_ X )
	ismri2dd.5	|- ( ph -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) )
Assertion	ismri2dd	|- ( ph -> S e. I )

Proof

Step	Hyp	Ref	Expression
1		ismri2.1	|- N = ( mrCls ` A )
2		ismri2.2	|- I = ( mrInd ` A )
3		ismri2d.3	|- ( ph -> A e. ( Moore ` X ) )
4		ismri2d.4	|- ( ph -> S C_ X )
5		ismri2dd.5	|- ( ph -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) )
6	1 2 3 4	ismri2d	|- ( ph -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
7	5 6	mpbird	|- ( ph -> S e. I )