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 ∈ C cls ⁡ 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 ∈ C cls ⁡ J ⁡ ⋂ C ⊆ cls ⁡ J ⁡ c
16 ssiin ⊢ cls ⁡ J ⁡ ⋂ C ⊆ ⋂ c ∈ C cls ⁡ J ⁡ c ↔ ∀ c ∈ C cls ⁡ J ⁡ ⋂ C ⊆ cls ⁡ J ⁡ c
17 15 16 sylibr ⊢ J ∈ Top ∧ C ⊆ 𝒫 X → cls ⁡ J ⁡ ⋂ C ⊆ ⋂ c ∈ C cls ⁡ J ⁡ c