# 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 𝑋 = 𝐽
Assertion clsndisj ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑈𝐽𝑃𝑈 ) ) → ( 𝑈𝑆 ) ≠ ∅ )

### Proof

Step Hyp Ref Expression
1 clscld.1 𝑋 = 𝐽
2 simp1 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐽 ∈ Top )
3 simp2 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆𝑋 )
4 1 clsss3 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
5 4 sseld ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑃𝑋 ) )
6 5 3impia ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑃𝑋 )
7 simp3 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
8 1 elcls ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥𝑆 ) ≠ ∅ ) ) )
9 8 biimpa ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥𝑆 ) ≠ ∅ ) )
10 2 3 6 7 9 syl31anc ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥𝑆 ) ≠ ∅ ) )
11 eleq2 ( 𝑥 = 𝑈 → ( 𝑃𝑥𝑃𝑈 ) )
12 ineq1 ( 𝑥 = 𝑈 → ( 𝑥𝑆 ) = ( 𝑈𝑆 ) )
13 12 neeq1d ( 𝑥 = 𝑈 → ( ( 𝑥𝑆 ) ≠ ∅ ↔ ( 𝑈𝑆 ) ≠ ∅ ) )
14 11 13 imbi12d ( 𝑥 = 𝑈 → ( ( 𝑃𝑥 → ( 𝑥𝑆 ) ≠ ∅ ) ↔ ( 𝑃𝑈 → ( 𝑈𝑆 ) ≠ ∅ ) ) )
15 14 rspccv ( ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥𝑆 ) ≠ ∅ ) → ( 𝑈𝐽 → ( 𝑃𝑈 → ( 𝑈𝑆 ) ≠ ∅ ) ) )
16 15 imp32 ( ( ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥𝑆 ) ≠ ∅ ) ∧ ( 𝑈𝐽𝑃𝑈 ) ) → ( 𝑈𝑆 ) ≠ ∅ )
17 10 16 sylan ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑈𝐽𝑃𝑈 ) ) → ( 𝑈𝑆 ) ≠ ∅ )