Metamath Proof Explorer

Theorem clsint2

Description: The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009)

Ref Expression
Hypothesis clsint2.1 ⊢X=⋃J
Assertion clsint2 ⊢J∈Top∧C⊆𝒫X→cls⁡J⁡⋂C⊆⋂c∈Ccls⁡J⁡c

Proof

Step Hyp Ref Expression
1 clsint2.1 ⊢X=⋃J
2 sspwuni ⊢C⊆𝒫X↔⋃C⊆X
3 elssuni ⊢c∈C→c⊆⋃C
4 sstr2 ⊢c⊆⋃C→⋃C⊆X→c⊆X
5 3 4 syl ⊢c∈C→⋃C⊆X→c⊆X
6 5 adantl ⊢J∈Top∧c∈C→⋃C⊆X→c⊆X
7 intss1 ⊢c∈C→⋂C⊆c
8 1 clsss ⊢J∈Top∧c⊆X∧⋂C⊆c→cls⁡J⁡⋂C⊆cls⁡J⁡c
9 7 8 syl3an3 ⊢J∈Top∧c⊆X∧c∈C→cls⁡J⁡⋂C⊆cls⁡J⁡c
10 9 3com23 ⊢J∈Top∧c∈C∧c⊆X→cls⁡J⁡⋂C⊆cls⁡J⁡c
11 10 3expia ⊢J∈Top∧c∈C→c⊆X→cls⁡J⁡⋂C⊆cls⁡J⁡c
12 6 11 syld ⊢J∈Top∧c∈C→⋃C⊆X→cls⁡J⁡⋂C⊆cls⁡J⁡c
13 12 impancom ⊢J∈Top∧⋃C⊆X→c∈C→cls⁡J⁡⋂C⊆cls⁡J⁡c
14 2 13 sylan2b ⊢J∈Top∧C⊆𝒫X→c∈C→cls⁡J⁡⋂C⊆cls⁡J⁡c
15 14 ralrimiv ⊢J∈Top∧C⊆𝒫X→∀c∈Ccls⁡J⁡⋂C⊆cls⁡J⁡c
16 ssiin ⊢cls⁡J⁡⋂C⊆⋂c∈Ccls⁡J⁡c↔∀c∈Ccls⁡J⁡⋂C⊆cls⁡J⁡c
17 15 16 sylibr ⊢J∈Top∧C⊆𝒫X→cls⁡J⁡⋂C⊆⋂c∈Ccls⁡J⁡c