MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mrieqv2d Structured version   Visualization version   GIF version

Theorem mrieqv2d 16493
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.)
Hypotheses
Ref Expression
mrieqvd.1 (𝜑𝐴 ∈ (Moore‘𝑋))
mrieqvd.2 𝑁 = (mrCls‘𝐴)
mrieqvd.3 𝐼 = (mrInd‘𝐴)
mrieqvd.4 (𝜑𝑆𝑋)
Assertion
Ref Expression
mrieqv2d (𝜑 → (𝑆𝐼 ↔ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))))
Distinct variable groups:   𝑆,𝑠   𝜑,𝑠   𝐼,𝑠   𝑁,𝑠
Allowed substitution hints:   𝐴(𝑠)   𝑋(𝑠)

Proof of Theorem mrieqv2d
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 pssnel 4175 . . . . . . 7 (𝑠𝑆 → ∃𝑥(𝑥𝑆 ∧ ¬ 𝑥𝑠))
213ad2ant3 1129 . . . . . 6 ((𝜑𝑆𝐼𝑠𝑆) → ∃𝑥(𝑥𝑆 ∧ ¬ 𝑥𝑠))
3 mrieqvd.1 . . . . . . . . . 10 (𝜑𝐴 ∈ (Moore‘𝑋))
433ad2ant1 1127 . . . . . . . . 9 ((𝜑𝑆𝐼𝑠𝑆) → 𝐴 ∈ (Moore‘𝑋))
54adantr 472 . . . . . . . 8 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝐴 ∈ (Moore‘𝑋))
6 mrieqvd.2 . . . . . . . 8 𝑁 = (mrCls‘𝐴)
7 simprr 813 . . . . . . . . . 10 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → ¬ 𝑥𝑠)
8 difsnb 4474 . . . . . . . . . 10 𝑥𝑠 ↔ (𝑠 ∖ {𝑥}) = 𝑠)
97, 8sylib 208 . . . . . . . . 9 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → (𝑠 ∖ {𝑥}) = 𝑠)
10 simpl3 1229 . . . . . . . . . . 11 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝑠𝑆)
1110pssssd 3838 . . . . . . . . . 10 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝑠𝑆)
1211ssdifd 3881 . . . . . . . . 9 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → (𝑠 ∖ {𝑥}) ⊆ (𝑆 ∖ {𝑥}))
139, 12eqsstr3d 3773 . . . . . . . 8 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝑠 ⊆ (𝑆 ∖ {𝑥}))
14 mrieqvd.3 . . . . . . . . . 10 𝐼 = (mrInd‘𝐴)
15 simpl2 1227 . . . . . . . . . 10 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝑆𝐼)
1614, 5, 15mrissd 16490 . . . . . . . . 9 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝑆𝑋)
1716ssdifssd 3883 . . . . . . . 8 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → (𝑆 ∖ {𝑥}) ⊆ 𝑋)
185, 6, 13, 17mrcssd 16478 . . . . . . 7 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → (𝑁𝑠) ⊆ (𝑁‘(𝑆 ∖ {𝑥})))
19 difssd 3873 . . . . . . . . 9 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → (𝑆 ∖ {𝑥}) ⊆ 𝑆)
205, 6, 19, 16mrcssd 16478 . . . . . . . 8 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊆ (𝑁𝑆))
215, 6, 16mrcssidd 16479 . . . . . . . . 9 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝑆 ⊆ (𝑁𝑆))
22 simprl 811 . . . . . . . . 9 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝑥𝑆)
2321, 22sseldd 3737 . . . . . . . 8 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → 𝑥 ∈ (𝑁𝑆))
246, 14, 5, 15, 22ismri2dad 16491 . . . . . . . 8 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))
2520, 23, 24ssnelpssd 3853 . . . . . . 7 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁𝑆))
2618, 25sspsstrd 3849 . . . . . 6 (((𝜑𝑆𝐼𝑠𝑆) ∧ (𝑥𝑆 ∧ ¬ 𝑥𝑠)) → (𝑁𝑠) ⊊ (𝑁𝑆))
272, 26exlimddv 2004 . . . . 5 ((𝜑𝑆𝐼𝑠𝑆) → (𝑁𝑠) ⊊ (𝑁𝑆))
28273expia 1114 . . . 4 ((𝜑𝑆𝐼) → (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)))
2928alrimiv 1996 . . 3 ((𝜑𝑆𝐼) → ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)))
3029ex 449 . 2 (𝜑 → (𝑆𝐼 → ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))))
313adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑆) → 𝐴 ∈ (Moore‘𝑋))
3231elfvexd 6375 . . . . . . . . . . . . 13 ((𝜑𝑥𝑆) → 𝑋 ∈ V)
33 mrieqvd.4 . . . . . . . . . . . . . 14 (𝜑𝑆𝑋)
3433adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑥𝑆) → 𝑆𝑋)
3532, 34ssexd 4949 . . . . . . . . . . . 12 ((𝜑𝑥𝑆) → 𝑆 ∈ V)
36 difexg 4952 . . . . . . . . . . . 12 (𝑆 ∈ V → (𝑆 ∖ {𝑥}) ∈ V)
3735, 36syl 17 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (𝑆 ∖ {𝑥}) ∈ V)
38 simp1r 1238 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → 𝑥𝑆)
39 difsnpss 4475 . . . . . . . . . . . . . . . 16 (𝑥𝑆 ↔ (𝑆 ∖ {𝑥}) ⊊ 𝑆)
4038, 39sylib 208 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑆 ∖ {𝑥}) ⊊ 𝑆)
41 simp2 1131 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → 𝑠 = (𝑆 ∖ {𝑥}))
4241psseq1d 3833 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑠𝑆 ↔ (𝑆 ∖ {𝑥}) ⊊ 𝑆))
4340, 42mpbird 247 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → 𝑠𝑆)
44 simp3 1132 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)))
4543, 44mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑁𝑠) ⊊ (𝑁𝑆))
4641fveq2d 6348 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑁𝑠) = (𝑁‘(𝑆 ∖ {𝑥})))
4746psseq1d 3833 . . . . . . . . . . . . 13 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → ((𝑁𝑠) ⊊ (𝑁𝑆) ↔ (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁𝑆)))
4845, 47mpbid 222 . . . . . . . . . . . 12 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥}) ∧ (𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁𝑆))
49483expia 1114 . . . . . . . . . . 11 (((𝜑𝑥𝑆) ∧ 𝑠 = (𝑆 ∖ {𝑥})) → ((𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁𝑆)))
5037, 49spcimdv 3422 . . . . . . . . . 10 ((𝜑𝑥𝑆) → (∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁𝑆)))
51503impia 1109 . . . . . . . . 9 ((𝜑𝑥𝑆 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ⊊ (𝑁𝑆))
5251pssned 3839 . . . . . . . 8 ((𝜑𝑥𝑆 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁𝑆))
53523com23 1120 . . . . . . 7 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) ∧ 𝑥𝑆) → (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁𝑆))
5433ad2ant1 1127 . . . . . . . . 9 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) ∧ 𝑥𝑆) → 𝐴 ∈ (Moore‘𝑋))
55333ad2ant1 1127 . . . . . . . . 9 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) ∧ 𝑥𝑆) → 𝑆𝑋)
56 simp3 1132 . . . . . . . . 9 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) ∧ 𝑥𝑆) → 𝑥𝑆)
5754, 6, 55, 56mrieqvlemd 16483 . . . . . . . 8 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) ∧ 𝑥𝑆) → (𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ (𝑁‘(𝑆 ∖ {𝑥})) = (𝑁𝑆)))
5857necon3bbid 2961 . . . . . . 7 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) ∧ 𝑥𝑆) → (¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁𝑆)))
5953, 58mpbird 247 . . . . . 6 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) ∧ 𝑥𝑆) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))
60593expia 1114 . . . . 5 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → (𝑥𝑆 → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))
6160ralrimiv 3095 . . . 4 ((𝜑 ∧ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))) → ∀𝑥𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))
6261ex 449 . . 3 (𝜑 → (∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) → ∀𝑥𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))
636, 14, 3, 33ismri2d 16487 . . 3 (𝜑 → (𝑆𝐼 ↔ ∀𝑥𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))
6462, 63sylibrd 249 . 2 (𝜑 → (∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) → 𝑆𝐼))
6530, 64impbid 202 1 (𝜑 → (𝑆𝐼 ↔ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072  wal 1622   = wceq 1624  wex 1845  wcel 2131  wne 2924  wral 3042  Vcvv 3332  cdif 3704  wss 3707  wpss 3708  {csn 4313  cfv 6041  Moorecmre 16436  mrClscmrc 16437  mrIndcmri 16438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-int 4620  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-fv 6049  df-mre 16440  df-mrc 16441  df-mri 16442
This theorem is referenced by:  mrissmrcd  16494
  Copyright terms: Public domain W3C validator