Theorem neindisj

Description: Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

	Ref	Expression
Hypothesis	neips.1	⊢ 𝑋 = ∪ 𝐽
Assertion	neindisj	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		neips.1	⊢ 𝑋 = ∪ 𝐽
2	1	clsss3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
3	2	sseld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑃 ∈ 𝑋 ) )
4	3	impr	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑃 ∈ 𝑋 )
5	1	isneip	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
6	4 5	syldan	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
7		3anass	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
8	1	clsndisj	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 ∈ 𝐽 ∧ 𝑃 ∈ 𝑔 ) ) → ( 𝑔 ∩ 𝑆 ) ≠ ∅ )
9	7 8	sylanbr	⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ∧ ( 𝑔 ∈ 𝐽 ∧ 𝑃 ∈ 𝑔 ) ) → ( 𝑔 ∩ 𝑆 ) ≠ ∅ )
10	9	anassrs	⊢ ( ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ∧ 𝑔 ∈ 𝐽 ) ∧ 𝑃 ∈ 𝑔 ) → ( 𝑔 ∩ 𝑆 ) ≠ ∅ )
11	10	adantllr	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑔 ∈ 𝐽 ) ∧ 𝑃 ∈ 𝑔 ) → ( 𝑔 ∩ 𝑆 ) ≠ ∅ )
12	11	adantrr	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑔 ∈ 𝐽 ) ∧ ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ( 𝑔 ∩ 𝑆 ) ≠ ∅ )
13		ssdisj	⊢ ( ( 𝑔 ⊆ 𝑁 ∧ ( 𝑁 ∩ 𝑆 ) = ∅ ) → ( 𝑔 ∩ 𝑆 ) = ∅ )
14	13	ex	⊢ ( 𝑔 ⊆ 𝑁 → ( ( 𝑁 ∩ 𝑆 ) = ∅ → ( 𝑔 ∩ 𝑆 ) = ∅ ) )
15	14	necon3d	⊢ ( 𝑔 ⊆ 𝑁 → ( ( 𝑔 ∩ 𝑆 ) ≠ ∅ → ( 𝑁 ∩ 𝑆 ) ≠ ∅ ) )
16	15	ad2antll	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑔 ∈ 𝐽 ) ∧ ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ( ( 𝑔 ∩ 𝑆 ) ≠ ∅ → ( 𝑁 ∩ 𝑆 ) ≠ ∅ ) )
17	12 16	mpd	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑔 ∈ 𝐽 ) ∧ ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ )
18	17	rexlimdva2	⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ∧ 𝑁 ⊆ 𝑋 ) → ( ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ ) )
19	18	expimpd	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ ) )
20	6 19	sylbid	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ ) )
21	20	exp32	⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ ) ) ) )
22	21	imp43	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ )