This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ) → ( 𝑈 ∩ 𝑆 ) ≠ ∅ )