Theorem clsval 22924

Description: The closure of a subset of a topology's base set is the intersection of all the closed sets that include it. Definition of closure of [Munkres] p. 94. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)

Hypothesis

Ref	Expression
iscld.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
clsval	⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥})

Distinct variable groups:   𝑥,𝐽   𝑥,𝑆   𝑥,𝑋

Proof of Theorem clsval

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iscld.1	. . . . 5 ⊢ 𝑋 = ∪ 𝐽
2	1	clsfval 22912	. . . 4 ⊢ (𝐽 ∈ Top → (cls‘𝐽) = (𝑦 ∈ 𝒫 𝑋 ↦ ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑦 ⊆ 𝑥}))
3	2	fveq1d 6860	. . 3 ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑆) = ((𝑦 ∈ 𝒫 𝑋 ↦ ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑦 ⊆ 𝑥})‘𝑆))
4	3	adantr 480	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ((𝑦 ∈ 𝒫 𝑋 ↦ ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑦 ⊆ 𝑥})‘𝑆))
5		eqid 2729	. . 3 ⊢ (𝑦 ∈ 𝒫 𝑋 ↦ ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑦 ⊆ 𝑥}) = (𝑦 ∈ 𝒫 𝑋 ↦ ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑦 ⊆ 𝑥})
6		sseq1 3972	. . . . 5 ⊢ (𝑦 = 𝑆 → (𝑦 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑥))
7	6	rabbidv 3413	. . . 4 ⊢ (𝑦 = 𝑆 → {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑦 ⊆ 𝑥} = {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥})
8	7	inteqd 4915	. . 3 ⊢ (𝑦 = 𝑆 → ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑦 ⊆ 𝑥} = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥})
9	1	topopn 22793	. . . . 5 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
10		elpw2g 5288	. . . . 5 ⊢ (𝑋 ∈ 𝐽 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
11	9, 10	syl 17	. . . 4 ⊢ (𝐽 ∈ Top → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
12	11	biimpar 477	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ 𝒫 𝑋)
13	1	topcld 22922	. . . . 5 ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
14		sseq2 3973	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑋))
15	14	rspcev 3588	. . . . 5 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑋) → ∃𝑥 ∈ (Clsd‘𝐽)𝑆 ⊆ 𝑥)
16	13, 15	sylan 580	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∃𝑥 ∈ (Clsd‘𝐽)𝑆 ⊆ 𝑥)
17		intexrab 5302	. . . 4 ⊢ (∃𝑥 ∈ (Clsd‘𝐽)𝑆 ⊆ 𝑥 ↔ ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥} ∈ V)
18	16, 17	sylib 218	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥} ∈ V)
19	5, 8, 12, 18	fvmptd3 6991	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑦 ∈ 𝒫 𝑋 ↦ ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑦 ⊆ 𝑥})‘𝑆) = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥})
20	4, 19	eqtrd 2764	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  {crab 3405  Vcvv 3447   ⊆ wss 3914  𝒫 cpw 4563  ∪ cuni 4871  ∩ cint 4910   ↦ cmpt 5188  ‘cfv 6511  Topctop 22780  Clsdccld 22903  clsccl 22905

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 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-top 22781  df-cld 22906  df-cls 22908

This theorem is referenced by:  cldcls  22929  clscld  22934  clsf  22935  clsval2  22937  clsss  22941  sscls  22943