# Metamath Proof Explorer

Description: Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses ismri2dad.1 ${⊢}{N}=\mathrm{mrCls}\left({A}\right)$
ismri2dad.2 ${⊢}{I}=\mathrm{mrInd}\left({A}\right)$
ismri2dad.3 ${⊢}{\phi }\to {A}\in \mathrm{Moore}\left({X}\right)$
ismri2dad.4 ${⊢}{\phi }\to {S}\in {I}$
ismri2dad.5 ${⊢}{\phi }\to {Y}\in {S}$
Assertion ismri2dad ${⊢}{\phi }\to ¬{Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 ismri2dad.1 ${⊢}{N}=\mathrm{mrCls}\left({A}\right)$
2 ismri2dad.2 ${⊢}{I}=\mathrm{mrInd}\left({A}\right)$
3 ismri2dad.3 ${⊢}{\phi }\to {A}\in \mathrm{Moore}\left({X}\right)$
4 ismri2dad.4 ${⊢}{\phi }\to {S}\in {I}$
5 ismri2dad.5 ${⊢}{\phi }\to {Y}\in {S}$
6 2 3 4 mrissd ${⊢}{\phi }\to {S}\subseteq {X}$
7 1 2 3 6 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)$
8 4 7 mpbid ${⊢}{\phi }\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)$
9 simpr ${⊢}\left({\phi }\wedge {x}={Y}\right)\to {x}={Y}$
10 9 sneqd ${⊢}\left({\phi }\wedge {x}={Y}\right)\to \left\{{x}\right\}=\left\{{Y}\right\}$
11 10 difeq2d ${⊢}\left({\phi }\wedge {x}={Y}\right)\to {S}\setminus \left\{{x}\right\}={S}\setminus \left\{{Y}\right\}$
12 11 fveq2d ${⊢}\left({\phi }\wedge {x}={Y}\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)={N}\left({S}\setminus \left\{{Y}\right\}\right)$
13 9 12 eleq12d ${⊢}\left({\phi }\wedge {x}={Y}\right)\to \left({x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)↔{Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)$
14 13 notbid ${⊢}\left({\phi }\wedge {x}={Y}\right)\to \left(¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)↔¬{Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)$
15 5 14 rspcdv ${⊢}{\phi }\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)\to ¬{Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)$
16 8 15 mpd ${⊢}{\phi }\to ¬{Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)$