Theorem sscls 22959

Description: A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)

Hypothesis

Ref	Expression
clscld.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
sscls	⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))

Proof of Theorem sscls

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssintub 4919	. 2 ⊢ 𝑆 ⊆ ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥}
2		clscld.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
3	2	clsval 22940	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥})
4	1, 3	sseqtrrid 3981	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3396   ⊆ wss 3905  ∪ cuni 4861  ∩ cint 4899  ‘cfv 6486  Topctop 22796  Clsdccld 22919  clsccl 22921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-top 22797  df-cld 22922  df-cls 22924

This theorem is referenced by:  iscld4  22968  elcls  22976  ntrcls0  22979  clslp  23051  restcls  23084  cncls2i  23173  nrmsep  23260  lpcls  23267  regsep2  23279  hauscmplem  23309  hauscmp  23310  clsconn  23333  conncompcld  23337  hausllycmp  23397  txcls  23507  ptclsg  23518  regr1lem  23642  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  fclscmpi  23932  flfcntr  23946  cnextfres  23972  clssubg  24012  tsmsid  24043  cnllycmp  24871  clsocv  25166  relcmpcmet  25234  bcthlem2  25241  bcthlem4  25243  limcnlp  25795  opnbnd  36298  opnregcld  36303  cldregopn  36304  heibor1lem  37788  heiborlem8  37797  sepdisj  48910  iscnrm3rlem4  48928