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 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
mrieqvd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
mrieqvd.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
mrieqvd.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
Assertion mrieqv2d ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 mrieqvd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mrieqvd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 mrieqvd.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4 mrieqvd.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
5 pssnel ⊢ ( 𝑠 ⊊ 𝑆 → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) )
6 5 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) )
7 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
8 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
9 simprr ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ¬ 𝑥 ∈ 𝑠 )
10 difsnb ⊢ ( ¬ 𝑥 ∈ 𝑠 ↔ ( 𝑠 ∖ { 𝑥 } ) = 𝑠 )
11 9 10 sylib ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ( 𝑠 ∖ { 𝑥 } ) = 𝑠 )
12 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝑠 ⊊ 𝑆 )
13 12 pssssd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝑠 ⊆ 𝑆 )
14 13 ssdifd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ( 𝑠 ∖ { 𝑥 } ) ⊆ ( 𝑆 ∖ { 𝑥 } ) )
15 11 14 eqsstrrd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝑠 ⊆ ( 𝑆 ∖ { 𝑥 } ) )
16 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝑆 ∈ 𝐼 )
17 3 8 16 mrissd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝑆 ⊆ 𝑋 )
18 17 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 )
19 8 2 15 18 mrcssd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ( 𝑁 ‘ 𝑠 ) ⊆ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
20 difssd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑆 )
21 8 2 20 17 mrcssd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ 𝑆 ) )
22 8 2 17 mrcssidd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝑆 ⊆ ( 𝑁 ‘ 𝑆 ) )
23 simprl ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ 𝑆 )
24 22 23 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ ( 𝑁 ‘ 𝑆 ) )
25 2 3 8 16 23 ismri2dad ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
26 21 24 25 ssnelpssd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊊ ( 𝑁 ‘ 𝑆 ) )
27 19 26 sspsstrd ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ¬ 𝑥 ∈ 𝑠 ) ) → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) )
28 6 27 exlimddv ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆 ) → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) )
29 28 3expia ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) → ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
30 29 alrimiv ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) → ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
31 30 ex ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 → ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) )
32 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
33 32 elfvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑋 ∈ V )
34 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ 𝑋 )
35 33 34 ssexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ∈ V )
36 35 difexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑆 ∖ { 𝑥 } ) ∈ V )
37 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → 𝑥 ∈ 𝑆 )
38 difsnpss ⊢ ( 𝑥 ∈ 𝑆 ↔ ( 𝑆 ∖ { 𝑥 } ) ⊊ 𝑆 )
39 37 38 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑆 ∖ { 𝑥 } ) ⊊ 𝑆 )
40 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → 𝑠 = ( 𝑆 ∖ { 𝑥 } ) )
41 40 psseq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑠 ⊊ 𝑆 ↔ ( 𝑆 ∖ { 𝑥 } ) ⊊ 𝑆 ) )
42 39 41 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → 𝑠 ⊊ 𝑆 )
43 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
44 42 43 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) )
45 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑁 ‘ 𝑠 ) = ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
46 45 psseq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ↔ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
47 44 46 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ∧ ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊊ ( 𝑁 ‘ 𝑆 ) )
48 47 3expia ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑠 = ( 𝑆 ∖ { 𝑥 } ) ) → ( ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
49 36 48 spcimdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
50 49 3impia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊊ ( 𝑁 ‘ 𝑆 ) )
51 50 pssned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ( 𝑁 ‘ 𝑆 ) )
52 51 3com23 ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ( 𝑁 ‘ 𝑆 ) )
53 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
54 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ 𝑋 )
55 simp3 ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
56 53 2 54 55 mrieqvlemd ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ 𝑆 ) ) )
57 56 necon3bbid ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ( 𝑁 ‘ 𝑆 ) ) )
58 52 57 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
59 58 3expia ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ( 𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
60 59 ralrimiv ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
61 60 ex ⊢ ( 𝜑 → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
62 2 3 1 4 ismri2d ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
63 61 62 sylibrd ⊢ ( 𝜑 → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) → 𝑆 ∈ 𝐼 ) )
64 31 63 impbid ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) )