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 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
mreexmrid.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
mreexmrid.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
mreexmrid.4 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
mreexmrid.5 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
mreexmrid.6 ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
mreexmrid.7 ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ 𝑆 ) )
Assertion mreexmrid ( 𝜑 → ( 𝑆 ∪ { 𝑌 } ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 mreexmrid.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mreexmrid.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 mreexmrid.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4 mreexmrid.4 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
5 mreexmrid.5 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
6 mreexmrid.6 ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
7 mreexmrid.7 ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ 𝑆 ) )
8 3 1 5 mrissd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
9 6 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑋 )
10 8 9 unssd ⊢ ( 𝜑 → ( 𝑆 ∪ { 𝑌 } ) ⊆ 𝑋 )
11 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
12 11 elfvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝑋 ∈ V )
13 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
14 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝑆 ∈ 𝐼 )
15 3 11 14 mrissd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝑆 ⊆ 𝑋 )
16 15 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 )
17 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝑌 ∈ 𝑋 )
18 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) )
19 difundir ⊢ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) = ( ( 𝑆 ∖ { 𝑥 } ) ∪ ( { 𝑌 } ∖ { 𝑥 } ) )
20 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝑥 ∈ 𝑆 )
21 1 2 8 mrcssidd ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑆 ) )
22 21 7 ssneldd ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝑆 )
23 22 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ¬ 𝑌 ∈ 𝑆 )
24 nelneq ⊢ ( ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑌 ∈ 𝑆 ) → ¬ 𝑥 = 𝑌 )
25 20 23 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ¬ 𝑥 = 𝑌 )
26 elsni ⊢ ( 𝑥 ∈ { 𝑌 } → 𝑥 = 𝑌 )
27 25 26 nsyl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ¬ 𝑥 ∈ { 𝑌 } )
28 difsnb ⊢ ( ¬ 𝑥 ∈ { 𝑌 } ↔ ( { 𝑌 } ∖ { 𝑥 } ) = { 𝑌 } )
29 27 28 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ( { 𝑌 } ∖ { 𝑥 } ) = { 𝑌 } )
30 29 uneq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ( ( 𝑆 ∖ { 𝑥 } ) ∪ ( { 𝑌 } ∖ { 𝑥 } ) ) = ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑌 } ) )
31 19 30 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) = ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑌 } ) )
32 31 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑌 } ) ) )
33 18 32 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑌 } ) ) )
34 2 3 11 14 20 ismri2dad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
35 12 13 16 17 33 34 mreexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) )
36 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ¬ 𝑌 ∈ ( 𝑁 ‘ 𝑆 ) )
37 undif1 ⊢ ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝑆 ∪ { 𝑥 } )
38 20 snssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → { 𝑥 } ⊆ 𝑆 )
39 ssequn2 ⊢ ( { 𝑥 } ⊆ 𝑆 ↔ ( 𝑆 ∪ { 𝑥 } ) = 𝑆 )
40 38 39 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ( 𝑆 ∪ { 𝑥 } ) = 𝑆 )
41 37 40 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝑆 )
42 41 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ( 𝑁 ‘ ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( 𝑁 ‘ 𝑆 ) )
43 36 42 neleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) → ¬ 𝑌 ∈ ( 𝑁 ‘ ( ( 𝑆 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) )
44 35 43 pm2.65i ⊢ ¬ ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) )
45 df-3an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) ) )
46 44 45 mtbi ⊢ ¬ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) )
47 46 imnani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) )
48 47 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ 𝑆 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) )
49 26 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → 𝑥 = 𝑌 )
50 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → ¬ 𝑌 ∈ ( 𝑁 ‘ 𝑆 ) )
51 49 50 eqneltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑆 ) )
52 49 sneqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → { 𝑥 } = { 𝑌 } )
53 52 difeq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) = ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑌 } ) )
54 difun2 ⊢ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑌 } ) = ( 𝑆 ∖ { 𝑌 } )
55 53 54 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) = ( 𝑆 ∖ { 𝑌 } ) )
56 difsnb ⊢ ( ¬ 𝑌 ∈ 𝑆 ↔ ( 𝑆 ∖ { 𝑌 } ) = 𝑆 )
57 22 56 sylib ⊢ ( 𝜑 → ( 𝑆 ∖ { 𝑌 } ) = 𝑆 )
58 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → ( 𝑆 ∖ { 𝑌 } ) = 𝑆 )
59 55 58 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) = 𝑆 )
60 59 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) = ( 𝑁 ‘ 𝑆 ) )
61 51 60 neleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) ∧ 𝑥 ∈ { 𝑌 } ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) )
62 elun ⊢ ( 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ↔ ( 𝑥 ∈ 𝑆 ∨ 𝑥 ∈ { 𝑌 } ) )
63 62 bilani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) → ( 𝑥 ∈ 𝑆 ∨ 𝑥 ∈ { 𝑌 } ) )
64 48 61 63 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) )
65 64 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑆 ∪ { 𝑌 } ) ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑆 ∪ { 𝑌 } ) ∖ { 𝑥 } ) ) )
66 2 3 1 10 65 ismri2dd ⊢ ( 𝜑 → ( 𝑆 ∪ { 𝑌 } ) ∈ 𝐼 )