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

Theorem clsss3 18790
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  |-  X  = 
U. J
Assertion
Ref Expression
clsss3  |-  ( ( J  e.  Top  /\  S  C_  X )  -> 
( ( cls `  J
) `  S )  C_  X )

Proof of Theorem clsss3
StepHypRef Expression
1 clscld.1 . . 3  |-  X  = 
U. J
21clscld 18778 . 2  |-  ( ( J  e.  Top  /\  S  C_  X )  -> 
( ( cls `  J
) `  S )  e.  ( Clsd `  J
) )
31cldss 18760 . 2  |-  ( ( ( cls `  J
) `  S )  e.  ( Clsd `  J
)  ->  ( ( cls `  J ) `  S )  C_  X
)
42, 3syl 16 1  |-  ( ( J  e.  Top  /\  S  C_  X )  -> 
( ( cls `  J
) `  S )  C_  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758    C_ wss 3431   U.cuni 4194   ` cfv 5521   Topctop 18625   Clsdccld 18747   clsccl 18749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4573  ax-pr 4634  ax-un 6477
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-ral 2801  df-rex 2802  df-reu 2803  df-rab 2805  df-v 3074  df-sbc 3289  df-csb 3391  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4195  df-int 4232  df-iun 4276  df-iin 4277  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-rn 4954  df-res 4955  df-ima 4956  df-iota 5484  df-fun 5523  df-fn 5524  df-f 5525  df-f1 5526  df-fo 5527  df-f1o 5528  df-fv 5529  df-top 18630  df-cld 18750  df-cls 18752
This theorem is referenced by:  cmntrcld  18794  clsidm  18798  elcls2  18805  clsndisj  18806  ntrcls0  18807  neindisj  18848  lpval  18870  lpss  18873  clslp  18879  cnclsi  19003  cncls  19005  isnrm2  19089  lpcls  19095  perfcls  19096  regsep2  19107  clscon  19161  concompcld  19165  2ndcsep  19190  1stcelcls  19192  hausllycmp  19225  txcls  19304  ptclsg  19315  imasncls  19392  kqnrmlem1  19443  reghmph  19493  nrmhmph  19494  flimclslem  19684  flimsncls  19686  hauspwpwf1  19687  fclsopn  19714  fclscmpi  19729  cnextfun  19763  clssubg  19806  clsnsg  19807  snclseqg  19813  utop3cls  19953  qdensere  20476  clsocv  20889  relcmpcmet  20954  cncmet  20960  kur14lem3  27235  topbnd  28662  clsun  28666  opnregcld  28668  cldregopn  28669  heibor1lem  28851
  Copyright terms: Public domain W3C validator