Theorem iscld 22970

Description: The predicate "the class 𝑆 is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)

Hypothesis

Ref	Expression
iscld.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
iscld	⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽)))

Proof of Theorem iscld

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iscld.1	. . . . 5 ⊢ 𝑋 = ∪ 𝐽
2	1	cldval 22966	. . . 4 ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ 𝐽})
3	2	eleq2d 2821	. . 3 ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ 𝑆 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ 𝐽}))
4		difeq2 4100	. . . . 5 ⊢ (𝑥 = 𝑆 → (𝑋 ∖ 𝑥) = (𝑋 ∖ 𝑆))
5	4	eleq1d 2820	. . . 4 ⊢ (𝑥 = 𝑆 → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (𝑋 ∖ 𝑆) ∈ 𝐽))
6	5	elrab 3676	. . 3 ⊢ (𝑆 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ 𝐽} ↔ (𝑆 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽))
7	3, 6	bitrdi 287	. 2 ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽)))
8	1	topopn 22849	. . . 4 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
9		elpw2g 5308	. . . 4 ⊢ (𝑋 ∈ 𝐽 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
10	8, 9	syl 17	. . 3 ⊢ (𝐽 ∈ Top → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
11	10	anbi1d 631	. 2 ⊢ (𝐽 ∈ Top → ((𝑆 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽)))
12	7, 11	bitrd 279	1 ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3420   ∖ cdif 3928   ⊆ wss 3931  𝒫 cpw 4580  ∪ cuni 4888  ‘cfv 6536  Topctop 22836  Clsdccld 22959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6538  df-fv 6544  df-top 22837  df-cld 22962

This theorem is referenced by:  iscld2  22971  cldss  22972  cldopn  22974  topcld  22978  discld  23032  indiscld  23034  restcld  23115  ordtcld1  23140  ordtcld2  23141  hauscmp  23350  txcld  23546  ptcld  23556  qtopcld  23656  opnsubg  24051  sszcld  24762  ist0cld  33869  stoweidlem57  46053