Theorem clsss3 23197

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 23185	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
3	1	cldss 23167	. 2 ⊢ (((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
4	2, 3	syl 18	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ⊆ wss 3906  ∪ cuni 4873  ‘cfv 6538  Topctop 23031  Clsdccld 23154  clsccl 23156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-int 4914  df-iun 4959  df-iin 4960  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-top 23032  df-cld 23157  df-cls 23159

This theorem is referenced by:  clsidm  23205  elcls2  23212  clsndisj  23213  ntrcls0  23214  neindisj  23255  lpval  23277  lpss  23280  clslp  23286  cnclsi  23410  cncls  23412  isnrm2  23496  lpcls  23502  perfcls  23503  regsep2  23514  clsconn  23568  conncompcld  23572  2ndcsep  23597  1stcelcls  23599  hausllycmp  23632  txcls  23742  ptclsg  23753  imasncls  23830  kqnrmlem1  23881  reghmph  23931  nrmhmph  23932  flimclslem  24122  flimsncls  24124  hauspwpwf1  24125  fclsopn  24152  fclscmpi  24167  cnextfun  24202  clssubg  24247  clsnsg  24248  snclseqg  24254  utop3cls  24389  qdensere  24907  clsocv  25390  relcmpcmet  25458  cncmet  25462  kur14lem3  35681  topbnd  36816  clsun  36820  opnregcld  36822  cldregopn  36823  heibor1lem  38441  qndenserrn  46996  iscnrm3rlem2  49702