# Metamath Proof Explorer

## Theorem ismri2d

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

Ref Expression
Hypotheses ismri2.1 ${⊢}{N}=\mathrm{mrCls}\left({A}\right)$
ismri2.2 ${⊢}{I}=\mathrm{mrInd}\left({A}\right)$
ismri2d.3 ${⊢}{\phi }\to {A}\in \mathrm{Moore}\left({X}\right)$
ismri2d.4 ${⊢}{\phi }\to {S}\subseteq {X}$
Assertion ismri2d ${⊢}{\phi }\to \left({S}\in {I}↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ismri2.1 ${⊢}{N}=\mathrm{mrCls}\left({A}\right)$
2 ismri2.2 ${⊢}{I}=\mathrm{mrInd}\left({A}\right)$
3 ismri2d.3 ${⊢}{\phi }\to {A}\in \mathrm{Moore}\left({X}\right)$
4 ismri2d.4 ${⊢}{\phi }\to {S}\subseteq {X}$
5 1 2 ismri2 ${⊢}\left({A}\in \mathrm{Moore}\left({X}\right)\wedge {S}\subseteq {X}\right)\to \left({S}\in {I}↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)\right)$
6 3 4 5 syl2anc ${⊢}{\phi }\to \left({S}\in {I}↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)\right)$