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 ( 𝜑 → ( 𝑆𝐼 ↔ ∀ 𝑠 ( 𝑠𝑆 → ( 𝑁𝑠 ) ⊊ ( 𝑁𝑆 ) ) ) )