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

Metamath Proof Explorer

Theorem islp2

Description: The predicate " P is a limit point of S " in terms of neighborhoods. Definition of limit point in Munkres p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods. (Contributed by NM, 26-Feb-2007) (Proof shortened by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis lpfval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion islp2 ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 islp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
3 2 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
4 ssdifss ⊢ ( 𝑆 ⊆ 𝑋 → ( 𝑆 ∖ { 𝑃 } ) ⊆ 𝑋 )
5 1 neindisj2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑃 } ) ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
6 4 5 syl3an2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
7 3 6 bitrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )