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

Theorem clscld 22382
Description: The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.)
Hypothesis
Ref Expression
clscld.1 𝑋 = 𝐽
Assertion
Ref Expression
clscld ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))

Proof of Theorem clscld
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 clscld.1 . . 3 𝑋 = 𝐽
21clsval 22372 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((cls‘𝐽)‘𝑆) = {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥})
31topcld 22370 . . . . . 6 (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
43anim1i 615 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑋 ∈ (Clsd‘𝐽) ∧ 𝑆𝑋))
5 sseq2 3968 . . . . . 6 (𝑥 = 𝑋 → (𝑆𝑥𝑆𝑋))
65elrab 3643 . . . . 5 (𝑋 ∈ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥} ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ 𝑆𝑋))
74, 6sylibr 233 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑋 ∈ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥})
87ne0d 4293 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥} ≠ ∅)
9 ssrab2 4035 . . 3 {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥} ⊆ (Clsd‘𝐽)
10 intcld 22375 . . 3 (({𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥} ≠ ∅ ∧ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥} ⊆ (Clsd‘𝐽)) → {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥} ∈ (Clsd‘𝐽))
118, 9, 10sylancl 586 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋) → {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥} ∈ (Clsd‘𝐽))
122, 11eqeltrd 2838 1 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wne 2941  {crab 3405  wss 3908  c0 4280   cuni 4863   cint 4905  cfv 6493  Topctop 22226  Clsdccld 22351  clsccl 22353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-iin 4955  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-top 22227  df-cld 22354  df-cls 22356
This theorem is referenced by:  clsf  22383  clsss3  22394  iscld3  22399  clsidm  22402  restcls  22516  cncls2i  22605  nrmsep  22692  lpcls  22699  regsep2  22711  hauscmplem  22741  hausllycmp  22829  txcls  22939  ptclsg  22950  regr1lem  23074  kqreglem1  23076  kqreglem2  23077  kqnrmlem1  23078  kqnrmlem2  23079  fclscmpi  23364  tgptsmscld  23486  cnllycmp  24303  clsocv  24598  cmpcmet  24667  cncmet  24670  limcnlp  25226  clsun  34767  cldregopn  34770  heibor1lem  36235  iscnrm3rlem2  46906  iscnrm3rlem5  46909
  Copyright terms: Public domain W3C validator