# 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}=\bigcup {J}$
Assertion clsval ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)=\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$

### Proof

Step Hyp Ref Expression
1 iscld.1 ${⊢}{X}=\bigcup {J}$
2 1 clsfval ${⊢}{J}\in \mathrm{Top}\to \mathrm{cls}\left({J}\right)=\left({y}\in 𝒫{X}⟼\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{y}\subseteq {x}\right\}\right)$
3 2 fveq1d ${⊢}{J}\in \mathrm{Top}\to \mathrm{cls}\left({J}\right)\left({S}\right)=\left({y}\in 𝒫{X}⟼\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{y}\subseteq {x}\right\}\right)\left({S}\right)$
4 3 adantr ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)=\left({y}\in 𝒫{X}⟼\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{y}\subseteq {x}\right\}\right)\left({S}\right)$
5 eqid ${⊢}\left({y}\in 𝒫{X}⟼\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{y}\subseteq {x}\right\}\right)=\left({y}\in 𝒫{X}⟼\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{y}\subseteq {x}\right\}\right)$
6 sseq1 ${⊢}{y}={S}\to \left({y}\subseteq {x}↔{S}\subseteq {x}\right)$
7 6 rabbidv ${⊢}{y}={S}\to \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{y}\subseteq {x}\right\}=\left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$
8 7 inteqd ${⊢}{y}={S}\to \bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{y}\subseteq {x}\right\}=\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$
9 1 topopn ${⊢}{J}\in \mathrm{Top}\to {X}\in {J}$
10 elpw2g ${⊢}{X}\in {J}\to \left({S}\in 𝒫{X}↔{S}\subseteq {X}\right)$
11 9 10 syl ${⊢}{J}\in \mathrm{Top}\to \left({S}\in 𝒫{X}↔{S}\subseteq {X}\right)$
12 11 biimpar ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\in 𝒫{X}$
13 1 topcld ${⊢}{J}\in \mathrm{Top}\to {X}\in \mathrm{Clsd}\left({J}\right)$
14 sseq2 ${⊢}{x}={X}\to \left({S}\subseteq {x}↔{S}\subseteq {X}\right)$
15 14 rspcev ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {X}\right)\to \exists {x}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq {x}$
16 13 15 sylan ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \exists {x}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq {x}$
17 intexrab ${⊢}\exists {x}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq {x}↔\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}\in \mathrm{V}$
18 16 17 sylib ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}\in \mathrm{V}$
19 5 8 12 18 fvmptd3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({y}\in 𝒫{X}⟼\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{y}\subseteq {x}\right\}\right)\left({S}\right)=\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$
20 4 19 eqtrd ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)=\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$