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 
|- ( ph -> A e. ( Moore ` X ) )
mrieqvd.2 
|- N = ( mrCls ` A )
mrieqvd.3 
|- I = ( mrInd ` A )
mrieqvd.4 
|- ( ph -> S C_ X )
Assertion mrieqv2d 
|- ( ph -> ( S e. I <-> A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) )

Proof

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