Theorem cldopn 22857

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	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
cldopn	⊢ (𝑆 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑆) ∈ 𝐽)

Proof of Theorem cldopn

Step	Hyp	Ref	Expression
1		cldrcl 22852	. 2 ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)
2		iscld.1	. . . 4 ⊢ 𝑋 = ∪ 𝐽
3	2	iscld 22853	. . 3 ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽)))
4	3	simplbda 499	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑆) ∈ 𝐽)
5	1, 4	mpancom 685	1 ⊢ (𝑆 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑆) ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ∖ cdif 3937   ⊆ wss 3940  ∪ cuni 4899  ‘cfv 6533  Topctop 22717  Clsdccld 22842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6485  df-fun 6535  df-fn 6536  df-fv 6541  df-top 22718  df-cld 22845

This theorem is referenced by:  difopn  22860  iincld  22865  uncld  22867  iuncld  22871  clsval2  22876  opncldf1  22910  opncldf3  22912  restcld  22998  lecldbas  23045  cnclima  23094  nrmsep2  23182  nrmsep  23183  regsep2  23202  cmpcld  23228  dfconn2  23245  txcld  23429  ptcld  23439  kqcldsat  23559  regr1lem  23565  filconn  23709  cldsubg  23937  limcnlp  25729  dvrec  25809  dvexp3  25832  lhop1lem  25868  abelth  26295  logdmopn  26499  lgamucov  26886  onsucconni  35812  onint1  35824  pibt2  36788  mblfinlem3  37017  mblfinlem4  37018  ismblfin  37019  dvtanlem  37027  dvasin  37062  dvacos  37063  dvreasin  37064  dvreacos  37065  fourierdlem62  45369  opncldeqv  47722  iscnrm3rlem5  47765