# Metamath Proof Explorer

## Theorem mrieqvlemd

Description: In a Moore system, if Y is a member of S , ( S \ { Y } ) and S have the same closure if and only if Y is in the closure of ( S \ { Y } ) . Used in the proof of mrieqvd and mrieqv2d . Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrieqvlemd.1 ${⊢}{\phi }\to {A}\in \mathrm{Moore}\left({X}\right)$
mrieqvlemd.2 ${⊢}{N}=\mathrm{mrCls}\left({A}\right)$
mrieqvlemd.3 ${⊢}{\phi }\to {S}\subseteq {X}$
mrieqvlemd.4 ${⊢}{\phi }\to {Y}\in {S}$
Assertion mrieqvlemd ${⊢}{\phi }\to \left({Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)↔{N}\left({S}\setminus \left\{{Y}\right\}\right)={N}\left({S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 mrieqvlemd.1 ${⊢}{\phi }\to {A}\in \mathrm{Moore}\left({X}\right)$
2 mrieqvlemd.2 ${⊢}{N}=\mathrm{mrCls}\left({A}\right)$
3 mrieqvlemd.3 ${⊢}{\phi }\to {S}\subseteq {X}$
4 mrieqvlemd.4 ${⊢}{\phi }\to {Y}\in {S}$
5 1 adantr ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {A}\in \mathrm{Moore}\left({X}\right)$
6 undif1 ${⊢}\left({S}\setminus \left\{{Y}\right\}\right)\cup \left\{{Y}\right\}={S}\cup \left\{{Y}\right\}$
7 3 adantr ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {S}\subseteq {X}$
8 7 ssdifssd ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {S}\setminus \left\{{Y}\right\}\subseteq {X}$
9 5 2 8 mrcssidd ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {S}\setminus \left\{{Y}\right\}\subseteq {N}\left({S}\setminus \left\{{Y}\right\}\right)$
10 simpr ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)$
11 10 snssd ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to \left\{{Y}\right\}\subseteq {N}\left({S}\setminus \left\{{Y}\right\}\right)$
12 9 11 unssd ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to \left({S}\setminus \left\{{Y}\right\}\right)\cup \left\{{Y}\right\}\subseteq {N}\left({S}\setminus \left\{{Y}\right\}\right)$
13 6 12 eqsstrrid ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {S}\cup \left\{{Y}\right\}\subseteq {N}\left({S}\setminus \left\{{Y}\right\}\right)$
14 13 unssad ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {S}\subseteq {N}\left({S}\setminus \left\{{Y}\right\}\right)$
15 difssd ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {S}\setminus \left\{{Y}\right\}\subseteq {S}$
16 5 2 14 15 mressmrcd ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {N}\left({S}\right)={N}\left({S}\setminus \left\{{Y}\right\}\right)$
17 16 eqcomd ${⊢}\left({\phi }\wedge {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)\right)\to {N}\left({S}\setminus \left\{{Y}\right\}\right)={N}\left({S}\right)$
18 1 2 3 mrcssidd ${⊢}{\phi }\to {S}\subseteq {N}\left({S}\right)$
19 18 4 sseldd ${⊢}{\phi }\to {Y}\in {N}\left({S}\right)$
20 19 adantr ${⊢}\left({\phi }\wedge {N}\left({S}\setminus \left\{{Y}\right\}\right)={N}\left({S}\right)\right)\to {Y}\in {N}\left({S}\right)$
21 simpr ${⊢}\left({\phi }\wedge {N}\left({S}\setminus \left\{{Y}\right\}\right)={N}\left({S}\right)\right)\to {N}\left({S}\setminus \left\{{Y}\right\}\right)={N}\left({S}\right)$
22 20 21 eleqtrrd ${⊢}\left({\phi }\wedge {N}\left({S}\setminus \left\{{Y}\right\}\right)={N}\left({S}\right)\right)\to {Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)$
23 17 22 impbida ${⊢}{\phi }\to \left({Y}\in {N}\left({S}\setminus \left\{{Y}\right\}\right)↔{N}\left({S}\setminus \left\{{Y}\right\}\right)={N}\left({S}\right)\right)$