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 e. ( Moore ` X ) /\ S C_ X ) -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )

Proof

Step Hyp Ref Expression
1 ismri2.1
 |-  N = ( mrCls ` A )
2 ismri2.2
 |-  I = ( mrInd ` A )
3 1 2 ismri
 |-  ( A e. ( Moore ` X ) -> ( S e. I <-> ( S C_ X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) )
4 3 baibd
 |-  ( ( A e. ( Moore ` X ) /\ S C_ X ) -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )