Metamath Proof Explorer

Theorem clsndisj

Description: Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of Munkres p. 95. (Contributed by NM, 26-Feb-2007)

Ref Expression
Hypothesis clscld.1 ⊢ X = ⋃ J
Assertion clsndisj ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S ∧ U ∈ J ∧ P ∈ U → U ∩ S ≠ ∅

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 simp1 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S → J ∈ Top
3 simp2 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S → S ⊆ X
4 1 clsss3 ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ S ⊆ X
5 4 sseld ⊢ J ∈ Top ∧ S ⊆ X → P ∈ cls ⁡ J ⁡ S → P ∈ X
6 5 3impia ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S → P ∈ X
7 simp3 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S → P ∈ cls ⁡ J ⁡ S
8 1 elcls ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ cls ⁡ J ⁡ S ↔ ∀ x ∈ J P ∈ x → x ∩ S ≠ ∅
9 8 biimpa ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X ∧ P ∈ cls ⁡ J ⁡ S → ∀ x ∈ J P ∈ x → x ∩ S ≠ ∅
10 2 3 6 7 9 syl31anc ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S → ∀ x ∈ J P ∈ x → x ∩ S ≠ ∅
11 eleq2 ⊢ x = U → P ∈ x ↔ P ∈ U
12 ineq1 ⊢ x = U → x ∩ S = U ∩ S
13 12 neeq1d ⊢ x = U → x ∩ S ≠ ∅ ↔ U ∩ S ≠ ∅
14 11 13 imbi12d ⊢ x = U → P ∈ x → x ∩ S ≠ ∅ ↔ P ∈ U → U ∩ S ≠ ∅
15 14 rspccv ⊢ ∀ x ∈ J P ∈ x → x ∩ S ≠ ∅ → U ∈ J → P ∈ U → U ∩ S ≠ ∅
16 15 imp32 ⊢ ∀ x ∈ J P ∈ x → x ∩ S ≠ ∅ ∧ U ∈ J ∧ P ∈ U → U ∩ S ≠ ∅
17 10 16 sylan ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S ∧ U ∈ J ∧ P ∈ U → U ∩ S ≠ ∅