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
|- ( 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 )