MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cldss Structured version   Unicode version

Theorem cldss 18655
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  |-  X  = 
U. J
Assertion
Ref Expression
cldss  |-  ( S  e.  ( Clsd `  J
)  ->  S  C_  X
)

Proof of Theorem cldss
StepHypRef Expression
1 cldrcl 18652 . 2  |-  ( S  e.  ( Clsd `  J
)  ->  J  e.  Top )
2 iscld.1 . . . 4  |-  X  = 
U. J
32iscld 18653 . . 3  |-  ( J  e.  Top  ->  ( S  e.  ( Clsd `  J )  <->  ( S  C_  X  /\  ( X 
\  S )  e.  J ) ) )
43simprbda 623 . 2  |-  ( ( J  e.  Top  /\  S  e.  ( Clsd `  J ) )  ->  S  C_  X )
51, 4mpancom 669 1  |-  ( S  e.  ( Clsd `  J
)  ->  S  C_  X
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756    \ cdif 3346    C_ wss 3349   U.cuni 4112   ` cfv 5439   Topctop 18520   Clsdccld 18642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-iota 5402  df-fun 5441  df-fn 5442  df-fv 5447  df-top 18525  df-cld 18645
This theorem is referenced by:  cldss2  18656  iincld  18665  uncld  18667  cldcls  18668  iuncld  18671  clsval2  18676  clsss3  18685  clsss2  18698  opncldf1  18710  restcldr  18800  lmcld  18929  nrmsep2  18982  nrmsep  18983  isnrm2  18984  regsep2  19002  cmpcld  19027  dfcon2  19045  concompclo  19061  cldllycmp  19121  txcld  19198  ptcld  19208  imasncld  19286  kqcldsat  19328  kqnrmlem1  19338  kqnrmlem2  19339  nrmhmph  19389  ufildr  19526  metnrmlem1a  20456  metnrmlem1  20457  metnrmlem2  20458  metnrmlem3  20459  cnheiborlem  20548  cmetss  20847  bcthlem5  20861  cldssbrsiga  26623  mblfinlem3  28456  mblfinlem4  28457  ismblfin  28458  clsun  28549  cldregopn  28552  cmpfiiin  29059  kelac1  29442  stoweidlem18  29839  stoweidlem57  29878
  Copyright terms: Public domain W3C validator