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

Theorem cldopn 19983
Description: The complement of a closed set is open. (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
cldopn  |-  ( S  e.  ( Clsd `  J
)  ->  ( X  \  S )  e.  J
)

Proof of Theorem cldopn
StepHypRef Expression
1 cldrcl 19978 . 2  |-  ( S  e.  ( Clsd `  J
)  ->  J  e.  Top )
2 iscld.1 . . . 4  |-  X  = 
U. J
32iscld 19979 . . 3  |-  ( J  e.  Top  ->  ( S  e.  ( Clsd `  J )  <->  ( S  C_  X  /\  ( X 
\  S )  e.  J ) ) )
43simplbda 628 . 2  |-  ( ( J  e.  Top  /\  S  e.  ( Clsd `  J ) )  -> 
( X  \  S
)  e.  J )
51, 4mpancom 673 1  |-  ( S  e.  ( Clsd `  J
)  ->  ( X  \  S )  e.  J
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872    \ cdif 3371    C_ wss 3374   U.cuni 4157   ` cfv 5539   Topctop 19854   Clsdccld 19968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-iota 5503  df-fun 5541  df-fn 5542  df-fv 5547  df-top 19858  df-cld 19971
This theorem is referenced by:  difopn  19986  iincld  19991  uncld  19993  iuncld  19997  clsval2  20002  opncldf1  20037  opncldf3  20039  restcld  20125  lecldbas  20172  cnclima  20221  nrmsep2  20309  nrmsep  20310  regsep2  20329  cmpcld  20354  dfcon2  20371  txcld  20555  ptcld  20565  kqcldsat  20685  regr1lem  20691  filcon  20835  cldsubg  21062  limcnlp  22770  dvrec  22846  dvexp3  22867  lhop1lem  22902  abelth  23333  logdmopn  23531  lgamucov  23900  onsucconi  31041  onint1  31053  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  dvtanlem  31897  dvtanlemOLD  31898  dvasin  31935  dvacos  31936  dvreasin  31937  dvreacos  31938  fourierdlem62  37915
  Copyright terms: Public domain W3C validator