Theorem clsss3 23049

Description: The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)

Hypothesis

Ref	Expression
clscld.1	⊢ 𝑋 = ∪ 𝐽

Assertion

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

Proof of Theorem clsss3

Step	Hyp	Ref	Expression
1		clscld.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
2	1	clscld 23037	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
3	1	cldss 23019	. 2 ⊢ (((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
4	2, 3	syl 17	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ⊆ wss 3890  ∪ cuni 4845  ‘cfv 6492  Topctop 22883  Clsdccld 23006  clsccl 23008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-iin 4931  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-top 22884  df-cld 23009  df-cls 23011

This theorem is referenced by:  clsidm  23057  elcls2  23064  clsndisj  23065  ntrcls0  23066  neindisj  23107  lpval  23129  lpss  23132  clslp  23138  cnclsi  23262  cncls  23264  isnrm2  23348  lpcls  23354  perfcls  23355  regsep2  23366  clsconn  23420  conncompcld  23424  2ndcsep  23449  1stcelcls  23451  hausllycmp  23484  txcls  23594  ptclsg  23605  imasncls  23682  kqnrmlem1  23733  reghmph  23783  nrmhmph  23784  flimclslem  23974  flimsncls  23976  hauspwpwf1  23977  fclsopn  24004  fclscmpi  24019  cnextfun  24054  clssubg  24099  clsnsg  24100  snclseqg  24106  utop3cls  24241  qdensere  24759  clsocv  25242  relcmpcmet  25310  cncmet  25314  kur14lem3  35443  topbnd  36559  clsun  36563  opnregcld  36565  cldregopn  36566  heibor1lem  38183  qndenserrn  46749  iscnrm3rlem2  49438