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

Theorem mrissmrcd 16970
 Description: In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd 16957, and so are equal by mrieqv2d 16969.) (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
mrissmrcd.1 (𝜑𝐴 ∈ (Moore‘𝑋))
mrissmrcd.2 𝑁 = (mrCls‘𝐴)
mrissmrcd.3 𝐼 = (mrInd‘𝐴)
mrissmrcd.4 (𝜑𝑆 ⊆ (𝑁𝑇))
mrissmrcd.5 (𝜑𝑇𝑆)
mrissmrcd.6 (𝜑𝑆𝐼)
Assertion
Ref Expression
mrissmrcd (𝜑𝑆 = 𝑇)

Proof of Theorem mrissmrcd
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 mrissmrcd.1 . . . . . 6 (𝜑𝐴 ∈ (Moore‘𝑋))
2 mrissmrcd.2 . . . . . 6 𝑁 = (mrCls‘𝐴)
3 mrissmrcd.4 . . . . . 6 (𝜑𝑆 ⊆ (𝑁𝑇))
4 mrissmrcd.5 . . . . . 6 (𝜑𝑇𝑆)
51, 2, 3, 4mressmrcd 16957 . . . . 5 (𝜑 → (𝑁𝑆) = (𝑁𝑇))
6 pssne 4003 . . . . . . 7 ((𝑁𝑇) ⊊ (𝑁𝑆) → (𝑁𝑇) ≠ (𝑁𝑆))
76necomd 3007 . . . . . 6 ((𝑁𝑇) ⊊ (𝑁𝑆) → (𝑁𝑆) ≠ (𝑁𝑇))
87necon2bi 2982 . . . . 5 ((𝑁𝑆) = (𝑁𝑇) → ¬ (𝑁𝑇) ⊊ (𝑁𝑆))
95, 8syl 17 . . . 4 (𝜑 → ¬ (𝑁𝑇) ⊊ (𝑁𝑆))
10 mrissmrcd.6 . . . . . 6 (𝜑𝑆𝐼)
11 mrissmrcd.3 . . . . . . 7 𝐼 = (mrInd‘𝐴)
1211, 1, 10mrissd 16966 . . . . . . 7 (𝜑𝑆𝑋)
131, 2, 11, 12mrieqv2d 16969 . . . . . 6 (𝜑 → (𝑆𝐼 ↔ ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆))))
1410, 13mpbid 235 . . . . 5 (𝜑 → ∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)))
1510, 4ssexd 5195 . . . . . 6 (𝜑𝑇 ∈ V)
16 simpr 489 . . . . . . . 8 ((𝜑𝑠 = 𝑇) → 𝑠 = 𝑇)
1716psseq1d 3999 . . . . . . 7 ((𝜑𝑠 = 𝑇) → (𝑠𝑆𝑇𝑆))
1816fveq2d 6663 . . . . . . . 8 ((𝜑𝑠 = 𝑇) → (𝑁𝑠) = (𝑁𝑇))
1918psseq1d 3999 . . . . . . 7 ((𝜑𝑠 = 𝑇) → ((𝑁𝑠) ⊊ (𝑁𝑆) ↔ (𝑁𝑇) ⊊ (𝑁𝑆)))
2017, 19imbi12d 349 . . . . . 6 ((𝜑𝑠 = 𝑇) → ((𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) ↔ (𝑇𝑆 → (𝑁𝑇) ⊊ (𝑁𝑆))))
2115, 20spcdv 3512 . . . . 5 (𝜑 → (∀𝑠(𝑠𝑆 → (𝑁𝑠) ⊊ (𝑁𝑆)) → (𝑇𝑆 → (𝑁𝑇) ⊊ (𝑁𝑆))))
2214, 21mpd 15 . . . 4 (𝜑 → (𝑇𝑆 → (𝑁𝑇) ⊊ (𝑁𝑆)))
239, 22mtod 201 . . 3 (𝜑 → ¬ 𝑇𝑆)
24 sspss 4006 . . . . 5 (𝑇𝑆 ↔ (𝑇𝑆𝑇 = 𝑆))
254, 24sylib 221 . . . 4 (𝜑 → (𝑇𝑆𝑇 = 𝑆))
2625ord 862 . . 3 (𝜑 → (¬ 𝑇𝑆𝑇 = 𝑆))
2723, 26mpd 15 . 2 (𝜑𝑇 = 𝑆)
2827eqcomd 2765 1 (𝜑𝑆 = 𝑇)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 845  ∀wal 1537   = wceq 1539   ∈ wcel 2112  Vcvv 3410   ⊆ wss 3859   ⊊ wpss 3860  ‘cfv 6336  Moorecmre 16912  mrClscmrc 16913  mrIndcmri 16914 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-int 4840  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-fv 6344  df-mre 16916  df-mrc 16917  df-mri 16918 This theorem is referenced by:  mreexexlem3d  16976  acsmap2d  17856
 Copyright terms: Public domain W3C validator