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

Metamath Proof Explorer

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 ‘ 𝐽 ) ‘ { 𝑃 } ) ) ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ )