Metamath Proof Explorer


Theorem mrissmrcd

Description: In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd , and so are equal by mrieqv2d .) (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrissmrcd.1 φAMooreX
mrissmrcd.2 N=mrClsA
mrissmrcd.3 I=mrIndA
mrissmrcd.4 φSNT
mrissmrcd.5 φTS
mrissmrcd.6 φSI
Assertion mrissmrcd φS=T

Proof

Step Hyp Ref Expression
1 mrissmrcd.1 φAMooreX
2 mrissmrcd.2 N=mrClsA
3 mrissmrcd.3 I=mrIndA
4 mrissmrcd.4 φSNT
5 mrissmrcd.5 φTS
6 mrissmrcd.6 φSI
7 1 2 4 5 mressmrcd φNS=NT
8 pssne NTNSNTNS
9 8 necomd NTNSNSNT
10 9 necon2bi NS=NT¬NTNS
11 7 10 syl φ¬NTNS
12 3 1 6 mrissd φSX
13 1 2 3 12 mrieqv2d φSIssSNsNS
14 6 13 mpbid φssSNsNS
15 6 5 ssexd φTV
16 simpr φs=Ts=T
17 16 psseq1d φs=TsSTS
18 16 fveq2d φs=TNs=NT
19 18 psseq1d φs=TNsNSNTNS
20 17 19 imbi12d φs=TsSNsNSTSNTNS
21 15 20 spcdv φssSNsNSTSNTNS
22 14 21 mpd φTSNTNS
23 11 22 mtod φ¬TS
24 sspss TSTST=S
25 5 24 sylib φTST=S
26 25 ord φ¬TST=S
27 23 26 mpd φT=S
28 27 eqcomd φS=T