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 ) ) ) )