Metamath Proof Explorer

Theorem mreexmrid

Description: In a Moore system whose closure operator has the exchange property, if a set is independent and an element is not in its closure, then adding the element to the set gives another independent set. Lemma 4.1.5 in FaureFrolicher p. 84. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexmrid.1 
|- ( ph -> A e. ( Moore ` X ) )
mreexmrid.2 
|- N = ( mrCls ` A )
mreexmrid.3 
|- I = ( mrInd ` A )
mreexmrid.4 
|- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
mreexmrid.5 
|- ( ph -> S e. I )
mreexmrid.6 
|- ( ph -> Y e. X )
mreexmrid.7 
|- ( ph -> -. Y e. ( N ` S ) )
Assertion mreexmrid 
|- ( ph -> ( S u. { Y } ) e. I )

Proof

Step Hyp Ref Expression
1 mreexmrid.1 
 |-  ( ph -> A e. ( Moore ` X ) )
2 mreexmrid.2 
 |-  N = ( mrCls ` A )
3 mreexmrid.3 
 |-  I = ( mrInd ` A )
4 mreexmrid.4 
 |-  ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
5 mreexmrid.5 
 |-  ( ph -> S e. I )
6 mreexmrid.6 
 |-  ( ph -> Y e. X )
7 mreexmrid.7 
 |-  ( ph -> -. Y e. ( N ` S ) )
8 3 1 5 mrissd 
 |-  ( ph -> S C_ X )
9 6 snssd 
 |-  ( ph -> { Y } C_ X )
10 8 9 unssd 
 |-  ( ph -> ( S u. { Y } ) C_ X )
11 1 3ad2ant1 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> A e. ( Moore ` X ) )
12 11 elfvexd 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> X e. _V )
13 4 3ad2ant1 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
14 5 3ad2ant1 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> S e. I )
15 3 11 14 mrissd 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> S C_ X )
16 15 ssdifssd 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> ( S \ { x } ) C_ X )
17 6 3ad2ant1 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> Y e. X )
18 simp3 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) )
19 difundir 
 |-  ( ( S u. { Y } ) \ { x } ) = ( ( S \ { x } ) u. ( { Y } \ { x } ) )
20 simp2 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> x e. S )
21 1 2 8 mrcssidd 
 |-  ( ph -> S C_ ( N ` S ) )
22 21 7 ssneldd 
 |-  ( ph -> -. Y e. S )
23 22 3ad2ant1 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> -. Y e. S )
24 nelneq 
 |-  ( ( x e. S /\ -. Y e. S ) -> -. x = Y )
25 20 23 24 syl2anc 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> -. x = Y )
26 elsni 
 |-  ( x e. { Y } -> x = Y )
27 25 26 nsyl 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> -. x e. { Y } )
28 difsnb 
 |-  ( -. x e. { Y } <-> ( { Y } \ { x } ) = { Y } )
29 27 28 sylib 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> ( { Y } \ { x } ) = { Y } )
30 29 uneq2d 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> ( ( S \ { x } ) u. ( { Y } \ { x } ) ) = ( ( S \ { x } ) u. { Y } ) )
31 19 30 syl5eq 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> ( ( S u. { Y } ) \ { x } ) = ( ( S \ { x } ) u. { Y } ) )
32 31 fveq2d 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> ( N ` ( ( S u. { Y } ) \ { x } ) ) = ( N ` ( ( S \ { x } ) u. { Y } ) ) )
33 18 32 eleqtrd 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> x e. ( N ` ( ( S \ { x } ) u. { Y } ) ) )
34 2 3 11 14 20 ismri2dad 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> -. x e. ( N ` ( S \ { x } ) ) )
35 12 13 16 17 33 34 mreexd 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> Y e. ( N ` ( ( S \ { x } ) u. { x } ) ) )
36 7 3ad2ant1 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> -. Y e. ( N ` S ) )
37 undif1 
 |-  ( ( S \ { x } ) u. { x } ) = ( S u. { x } )
38 20 snssd 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> { x } C_ S )
39 ssequn2 
 |-  ( { x } C_ S <-> ( S u. { x } ) = S )
40 38 39 sylib 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> ( S u. { x } ) = S )
41 37 40 syl5eq 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> ( ( S \ { x } ) u. { x } ) = S )
42 41 fveq2d 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> ( N ` ( ( S \ { x } ) u. { x } ) ) = ( N ` S ) )
43 36 42 neleqtrrd 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) -> -. Y e. ( N ` ( ( S \ { x } ) u. { x } ) ) )
44 35 43 pm2.65i 
 |-  -. ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) )
45 df-3an 
 |-  ( ( ph /\ x e. S /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) <-> ( ( ph /\ x e. S ) /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) ) )
46 44 45 mtbi 
 |-  -. ( ( ph /\ x e. S ) /\ x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) )
47 46 imnani 
 |-  ( ( ph /\ x e. S ) -> -. x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) )
48 47 adantlr 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. S ) -> -. x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) )
49 26 adantl 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> x = Y )
50 7 ad2antrr 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> -. Y e. ( N ` S ) )
51 49 50 eqneltrd 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> -. x e. ( N ` S ) )
52 49 sneqd 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> { x } = { Y } )
53 52 difeq2d 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> ( ( S u. { Y } ) \ { x } ) = ( ( S u. { Y } ) \ { Y } ) )
54 difun2 
 |-  ( ( S u. { Y } ) \ { Y } ) = ( S \ { Y } )
55 53 54 eqtrdi 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> ( ( S u. { Y } ) \ { x } ) = ( S \ { Y } ) )
56 difsnb 
 |-  ( -. Y e. S <-> ( S \ { Y } ) = S )
57 22 56 sylib 
 |-  ( ph -> ( S \ { Y } ) = S )
58 57 ad2antrr 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> ( S \ { Y } ) = S )
59 55 58 eqtrd 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> ( ( S u. { Y } ) \ { x } ) = S )
60 59 fveq2d 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> ( N ` ( ( S u. { Y } ) \ { x } ) ) = ( N ` S ) )
61 51 60 neleqtrrd 
 |-  ( ( ( ph /\ x e. ( S u. { Y } ) ) /\ x e. { Y } ) -> -. x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) )
62 simpr 
 |-  ( ( ph /\ x e. ( S u. { Y } ) ) -> x e. ( S u. { Y } ) )
63 elun 
 |-  ( x e. ( S u. { Y } ) <-> ( x e. S \/ x e. { Y } ) )
64 62 63 sylib 
 |-  ( ( ph /\ x e. ( S u. { Y } ) ) -> ( x e. S \/ x e. { Y } ) )
65 48 61 64 mpjaodan 
 |-  ( ( ph /\ x e. ( S u. { Y } ) ) -> -. x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) )
66 65 ralrimiva 
 |-  ( ph -> A. x e. ( S u. { Y } ) -. x e. ( N ` ( ( S u. { Y } ) \ { x } ) ) )
67 2 3 1 10 66 ismri2dd 
 |-  ( ph -> ( S u. { Y } ) e. I )