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