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 35 difexd 
 |-  ( ( ph /\ x e. S ) -> ( S \ { x } ) e. _V )
37 simp1r 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> x e. S )
38 difsnpss 
 |-  ( x e. S <-> ( S \ { x } ) C. S )
39 37 38 sylib 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( S \ { x } ) C. S )
40 simp2 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> s = ( S \ { x } ) )
41 40 psseq1d 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( s C. S <-> ( S \ { x } ) C. S ) )
42 39 41 mpbird 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> s C. S )
43 simp3 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( s C. S -> ( N ` s ) C. ( N ` S ) ) )
44 42 43 mpd 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( N ` s ) C. ( N ` S ) )
45 40 fveq2d 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( N ` s ) = ( N ` ( S \ { x } ) ) )
46 45 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 ) ) )
47 44 46 mpbid 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) /\ ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( N ` ( S \ { x } ) ) C. ( N ` S ) )
48 47 3expia 
 |-  ( ( ( ph /\ x e. S ) /\ s = ( S \ { x } ) ) -> ( ( s C. S -> ( N ` s ) C. ( N ` S ) ) -> ( N ` ( S \ { x } ) ) C. ( N ` S ) ) )
49 36 48 spcimdv 
 |-  ( ( ph /\ x e. S ) -> ( A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) -> ( N ` ( S \ { x } ) ) C. ( N ` S ) ) )
50 49 3impia 
 |-  ( ( ph /\ x e. S /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( N ` ( S \ { x } ) ) C. ( N ` S ) )
51 50 pssned 
 |-  ( ( ph /\ x e. S /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( N ` ( S \ { x } ) ) =/= ( N ` S ) )
52 51 3com23 
 |-  ( ( ph /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) /\ x e. S ) -> ( N ` ( S \ { x } ) ) =/= ( N ` S ) )
53 1 3ad2ant1 
 |-  ( ( ph /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) /\ x e. S ) -> A e. ( Moore ` X ) )
54 4 3ad2ant1 
 |-  ( ( ph /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) /\ x e. S ) -> S C_ X )
55 simp3 
 |-  ( ( ph /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) /\ x e. S ) -> x e. S )
56 53 2 54 55 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 ) ) )
57 56 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 ) ) )
58 52 57 mpbird 
 |-  ( ( ph /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) /\ x e. S ) -> -. x e. ( N ` ( S \ { x } ) ) )
59 58 3expia 
 |-  ( ( ph /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> ( x e. S -> -. x e. ( N ` ( S \ { x } ) ) ) )
60 59 ralrimiv 
 |-  ( ( ph /\ A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) )
61 60 ex 
 |-  ( ph -> ( A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
62 2 3 1 4 ismri2d 
 |-  ( ph -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
63 61 62 sylibrd 
 |-  ( ph -> ( A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) -> S e. I ) )
64 31 63 impbid 
 |-  ( ph -> ( S e. I <-> A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) )