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

Theorem cldss 19400
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 19397 . 2  |-  ( S  e.  ( Clsd `  J
)  ->  J  e.  Top )
2 iscld.1 . . . 4  |-  X  = 
U. J
32iscld 19398 . . 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 1381    e. wcel 1802    \ cdif 3456    C_ wss 3459   U.cuni 4231   ` cfv 5575   Topctop 19264   Clsdccld 19387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-mpt 4494  df-id 4782  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-iota 5538  df-fun 5577  df-fn 5578  df-fv 5583  df-top 19269  df-cld 19390
This theorem is referenced by:  cldss2  19401  iincld  19410  uncld  19412  cldcls  19413  iuncld  19416  clsval2  19421  clsss3  19430  clsss2  19443  opncldf1  19455  restcldr  19545  lmcld  19674  nrmsep2  19727  nrmsep  19728  isnrm2  19729  regsep2  19747  cmpcld  19772  dfcon2  19790  concompclo  19806  cldllycmp  19866  txcld  19974  ptcld  19984  imasncld  20062  kqcldsat  20104  kqnrmlem1  20114  kqnrmlem2  20115  nrmhmph  20165  ufildr  20302  metnrmlem1a  21232  metnrmlem1  21233  metnrmlem2  21234  metnrmlem3  21235  cnheiborlem  21324  cmetss  21623  bcthlem5  21637  cldssbrsiga  28028  mblfinlem3  30025  mblfinlem4  30026  ismblfin  30027  clsun  30118  cldregopn  30121  cmpfiiin  30601  kelac1  30981  stoweidlem18  31689  stoweidlem57  31728
  Copyright terms: Public domain W3C validator