Metamath Proof Explorer


Theorem clsval

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)

Ref Expression
Hypothesis iscld.1 X=J
Assertion clsval JTopSXclsJS=xClsdJ|Sx

Proof

Step Hyp Ref Expression
1 iscld.1 X=J
2 1 clsfval JTopclsJ=y𝒫XxClsdJ|yx
3 2 fveq1d JTopclsJS=y𝒫XxClsdJ|yxS
4 3 adantr JTopSXclsJS=y𝒫XxClsdJ|yxS
5 eqid y𝒫XxClsdJ|yx=y𝒫XxClsdJ|yx
6 sseq1 y=SyxSx
7 6 rabbidv y=SxClsdJ|yx=xClsdJ|Sx
8 7 inteqd y=SxClsdJ|yx=xClsdJ|Sx
9 1 topopn JTopXJ
10 elpw2g XJS𝒫XSX
11 9 10 syl JTopS𝒫XSX
12 11 biimpar JTopSXS𝒫X
13 1 topcld JTopXClsdJ
14 sseq2 x=XSxSX
15 14 rspcev XClsdJSXxClsdJSx
16 13 15 sylan JTopSXxClsdJSx
17 intexrab xClsdJSxxClsdJ|SxV
18 16 17 sylib JTopSXxClsdJ|SxV
19 5 8 12 18 fvmptd3 JTopSXy𝒫XxClsdJ|yxS=xClsdJ|Sx
20 4 19 eqtrd JTopSXclsJS=xClsdJ|Sx