# Metamath Proof Explorer

## Theorem mrieqv2d

Description: In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in FaureFrolicher p. 83. (Contributed by David Moews, 1-May-2017)

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

### Proof

Step Hyp Ref Expression
1 mrieqvd.1 ${⊢}{\phi }\to {A}\in \mathrm{Moore}\left({X}\right)$
2 mrieqvd.2 ${⊢}{N}=\mathrm{mrCls}\left({A}\right)$
3 mrieqvd.3 ${⊢}{I}=\mathrm{mrInd}\left({A}\right)$
4 mrieqvd.4 ${⊢}{\phi }\to {S}\subseteq {X}$
5 pssnel ${⊢}{s}\subset {S}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}\wedge ¬{x}\in {s}\right)$
6 5 3ad2ant3 ${⊢}\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}\wedge ¬{x}\in {s}\right)$
7 1 3ad2ant1 ${⊢}\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\to {A}\in \mathrm{Moore}\left({X}\right)$
8 7 adantr ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {A}\in \mathrm{Moore}\left({X}\right)$
9 simprr ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to ¬{x}\in {s}$
10 difsnb ${⊢}¬{x}\in {s}↔{s}\setminus \left\{{x}\right\}={s}$
11 9 10 sylib ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {s}\setminus \left\{{x}\right\}={s}$
12 simpl3 ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {s}\subset {S}$
13 12 pssssd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {s}\subseteq {S}$
14 13 ssdifd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {s}\setminus \left\{{x}\right\}\subseteq {S}\setminus \left\{{x}\right\}$
15 11 14 eqsstrrd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {s}\subseteq {S}\setminus \left\{{x}\right\}$
16 simpl2 ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {S}\in {I}$
17 3 8 16 mrissd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {S}\subseteq {X}$
18 17 ssdifssd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {S}\setminus \left\{{x}\right\}\subseteq {X}$
19 8 2 15 18 mrcssd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {N}\left({s}\right)\subseteq {N}\left({S}\setminus \left\{{x}\right\}\right)$
20 difssd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {S}\setminus \left\{{x}\right\}\subseteq {S}$
21 8 2 20 17 mrcssd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)\subseteq {N}\left({S}\right)$
22 8 2 17 mrcssidd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {S}\subseteq {N}\left({S}\right)$
23 simprl ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {x}\in {S}$
24 22 23 sseldd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {x}\in {N}\left({S}\right)$
25 2 3 8 16 23 ismri2dad ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to ¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)$
26 21 24 25 ssnelpssd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)\subset {N}\left({S}\right)$
27 19 26 sspsstrd ${⊢}\left(\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\wedge \left({x}\in {S}\wedge ¬{x}\in {s}\right)\right)\to {N}\left({s}\right)\subset {N}\left({S}\right)$
28 6 27 exlimddv ${⊢}\left({\phi }\wedge {S}\in {I}\wedge {s}\subset {S}\right)\to {N}\left({s}\right)\subset {N}\left({S}\right)$
29 28 3expia ${⊢}\left({\phi }\wedge {S}\in {I}\right)\to \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)$
30 29 alrimiv ${⊢}\left({\phi }\wedge {S}\in {I}\right)\to \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)$
31 30 ex ${⊢}{\phi }\to \left({S}\in {I}\to \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)$
32 1 adantr ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {A}\in \mathrm{Moore}\left({X}\right)$
33 32 elfvexd ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {X}\in \mathrm{V}$
34 4 adantr ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {S}\subseteq {X}$
35 33 34 ssexd ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {S}\in \mathrm{V}$
36 difexg ${⊢}{S}\in \mathrm{V}\to {S}\setminus \left\{{x}\right\}\in \mathrm{V}$
37 35 36 syl ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {S}\setminus \left\{{x}\right\}\in \mathrm{V}$
38 simp1r ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {x}\in {S}$
39 difsnpss ${⊢}{x}\in {S}↔{S}\setminus \left\{{x}\right\}\subset {S}$
40 38 39 sylib ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {S}\setminus \left\{{x}\right\}\subset {S}$
41 simp2 ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {s}={S}\setminus \left\{{x}\right\}$
42 41 psseq1d ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to \left({s}\subset {S}↔{S}\setminus \left\{{x}\right\}\subset {S}\right)$
43 40 42 mpbird ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {s}\subset {S}$
44 simp3 ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)$
45 43 44 mpd ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {N}\left({s}\right)\subset {N}\left({S}\right)$
46 41 fveq2d ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {N}\left({s}\right)={N}\left({S}\setminus \left\{{x}\right\}\right)$
47 46 psseq1d ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to \left({N}\left({s}\right)\subset {N}\left({S}\right)↔{N}\left({S}\setminus \left\{{x}\right\}\right)\subset {N}\left({S}\right)\right)$
48 45 47 mpbid ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\wedge \left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)\subset {N}\left({S}\right)$
49 48 3expia ${⊢}\left(\left({\phi }\wedge {x}\in {S}\right)\wedge {s}={S}\setminus \left\{{x}\right\}\right)\to \left(\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)\subset {N}\left({S}\right)\right)$
50 37 49 spcimdv ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to \left(\forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)\subset {N}\left({S}\right)\right)$
51 50 3impia ${⊢}\left({\phi }\wedge {x}\in {S}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)\subset {N}\left({S}\right)$
52 51 pssned ${⊢}\left({\phi }\wedge {x}\in {S}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)\ne {N}\left({S}\right)$
53 52 3com23 ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\wedge {x}\in {S}\right)\to {N}\left({S}\setminus \left\{{x}\right\}\right)\ne {N}\left({S}\right)$
54 1 3ad2ant1 ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\wedge {x}\in {S}\right)\to {A}\in \mathrm{Moore}\left({X}\right)$
55 4 3ad2ant1 ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\wedge {x}\in {S}\right)\to {S}\subseteq {X}$
56 simp3 ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\wedge {x}\in {S}\right)\to {x}\in {S}$
57 54 2 55 56 mrieqvlemd ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\wedge {x}\in {S}\right)\to \left({x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)↔{N}\left({S}\setminus \left\{{x}\right\}\right)={N}\left({S}\right)\right)$
58 57 necon3bbid ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\wedge {x}\in {S}\right)\to \left(¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)↔{N}\left({S}\setminus \left\{{x}\right\}\right)\ne {N}\left({S}\right)\right)$
59 53 58 mpbird ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\wedge {x}\in {S}\right)\to ¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)$
60 59 3expia ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to \left({x}\in {S}\to ¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)\right)$
61 60 ralrimiv ${⊢}\left({\phi }\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)$
62 61 ex ${⊢}{\phi }\to \left(\forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({S}\setminus \left\{{x}\right\}\right)\right)$
63 2 3 1 4 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)$
64 62 63 sylibrd ${⊢}{\phi }\to \left(\forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\to {S}\in {I}\right)$
65 31 64 impbid ${⊢}{\phi }\to \left({S}\in {I}↔\forall {s}\phantom{\rule{.4em}{0ex}}\left({s}\subset {S}\to {N}\left({s}\right)\subset {N}\left({S}\right)\right)\right)$