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 | |
|
Assertion | clsval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscld.1 | |
|
2 | 1 | clsfval | |
3 | 2 | fveq1d | |
4 | 3 | adantr | |
5 | eqid | |
|
6 | sseq1 | |
|
7 | 6 | rabbidv | |
8 | 7 | inteqd | |
9 | 1 | topopn | |
10 | elpw2g | |
|
11 | 9 10 | syl | |
12 | 11 | biimpar | |
13 | 1 | topcld | |
14 | sseq2 | |
|
15 | 14 | rspcev | |
16 | 13 15 | sylan | |
17 | intexrab | |
|
18 | 16 17 | sylib | |
19 | 5 8 12 18 | fvmptd3 | |
20 | 4 19 | eqtrd | |