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 
|- ( ph -> A e. ( Moore ` X ) )
mrissmrcd.2 
|- N = ( mrCls ` A )
mrissmrcd.3 
|- I = ( mrInd ` A )
mrissmrcd.4 
|- ( ph -> S C_ ( N ` T ) )
mrissmrcd.5 
|- ( ph -> T C_ S )
mrissmrcd.6 
|- ( ph -> S e. I )
Assertion mrissmrcd 
|- ( ph -> S = T )

Proof

Step Hyp Ref Expression
1 mrissmrcd.1 
 |-  ( ph -> A e. ( Moore ` X ) )
2 mrissmrcd.2 
 |-  N = ( mrCls ` A )
3 mrissmrcd.3 
 |-  I = ( mrInd ` A )
4 mrissmrcd.4 
 |-  ( ph -> S C_ ( N ` T ) )
5 mrissmrcd.5 
 |-  ( ph -> T C_ S )
6 mrissmrcd.6 
 |-  ( ph -> S e. I )
7 1 2 4 5 mressmrcd 
 |-  ( ph -> ( N ` S ) = ( N ` T ) )
8 pssne 
 |-  ( ( N ` T ) C. ( N ` S ) -> ( N ` T ) =/= ( N ` S ) )
9 8 necomd 
 |-  ( ( N ` T ) C. ( N ` S ) -> ( N ` S ) =/= ( N ` T ) )
10 9 necon2bi 
 |-  ( ( N ` S ) = ( N ` T ) -> -. ( N ` T ) C. ( N ` S ) )
11 7 10 syl 
 |-  ( ph -> -. ( N ` T ) C. ( N ` S ) )
12 3 1 6 mrissd 
 |-  ( ph -> S C_ X )
13 1 2 3 12 mrieqv2d 
 |-  ( ph -> ( S e. I <-> A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) )
14 6 13 mpbid 
 |-  ( ph -> A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) )
15 6 5 ssexd 
 |-  ( ph -> T e. _V )
16 simpr 
 |-  ( ( ph /\ s = T ) -> s = T )
17 16 psseq1d 
 |-  ( ( ph /\ s = T ) -> ( s C. S <-> T C. S ) )
18 16 fveq2d 
 |-  ( ( ph /\ s = T ) -> ( N ` s ) = ( N ` T ) )
19 18 psseq1d 
 |-  ( ( ph /\ s = T ) -> ( ( N ` s ) C. ( N ` S ) <-> ( N ` T ) C. ( N ` S ) ) )
20 17 19 imbi12d 
 |-  ( ( ph /\ s = T ) -> ( ( s C. S -> ( N ` s ) C. ( N ` S ) ) <-> ( T C. S -> ( N ` T ) C. ( N ` S ) ) ) )
21 15 20 spcdv 
 |-  ( ph -> ( A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) -> ( T C. S -> ( N ` T ) C. ( N ` S ) ) ) )
22 14 21 mpd 
 |-  ( ph -> ( T C. S -> ( N ` T ) C. ( N ` S ) ) )
23 11 22 mtod 
 |-  ( ph -> -. T C. S )
24 sspss 
 |-  ( T C_ S <-> ( T C. S \/ T = S ) )
25 5 24 sylib 
 |-  ( ph -> ( T C. S \/ T = S ) )
26 25 ord 
 |-  ( ph -> ( -. T C. S -> T = S ) )
27 23 26 mpd 
 |-  ( ph -> T = S )
28 27 eqcomd 
 |-  ( ph -> S = T )