Theorem cldss 20924

Description: A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)

Hypothesis

Ref	Expression
iscld.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
cldss	⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋)

Proof of Theorem cldss

Step	Hyp	Ref	Expression
1		cldrcl 20921	. 2 ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)
2		iscld.1	. . . 4 ⊢ 𝑋 = ∪ 𝐽
3	2	iscld 20922	. . 3 ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽)))
4	3	simprbda 654	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ⊆ 𝑋)
5	1, 4	mpancom 706	1 ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋)

Syntax hints:   → wi 4   = wceq 1564   ∈ wcel 2071   ∖ cdif 3645   ⊆ wss 3648  ∪ cuni 4512  ‘cfv 5969  Topctop 20789  Clsdccld 20911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-ral 2987  df-rex 2988  df-rab 2991  df-v 3274  df-sbc 3510  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-op 4260  df-uni 4513  df-br 4729  df-opab 4789  df-mpt 4806  df-id 5096  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-iota 5932  df-fun 5971  df-fn 5972  df-fv 5977  df-top 20790  df-cld 20914

This theorem is referenced by:  cldss2  20925  iincld  20934  uncld  20936  cldcls  20937  iuncld  20940  clsval2  20945  clsss3  20954  clsss2  20967  opncldf1  20979  restcldr  21069  lmcld  21198  nrmsep2  21251  nrmsep  21252  isnrm2  21253  regsep2  21271  cmpcld  21296  dfconn2  21313  conncompclo  21329  cldllycmp  21389  txcld  21497  ptcld  21507  imasncld  21585  kqcldsat  21627  kqnrmlem1  21637  kqnrmlem2  21638  nrmhmph  21688  ufildr  21825  metnrmlem1a  22751  metnrmlem1  22752  metnrmlem2  22753  metnrmlem3  22754  cnheiborlem  22843  cmetss  23202  bcthlem5  23214  cldssbrsiga  30448  clsun  32518  cldregopn  32521  mblfinlem3  33648  mblfinlem4  33649  ismblfin  33650  cmpfiiin  37647  kelac1  38020  stoweidlem18  40623  stoweidlem57  40662