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 ⊢ X = ⋃ J
Assertion islp2 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ limPt ⁡ J ⁡ S ↔ ∀ n ∈ nei ⁡ J ⁡ P n ∩ S ∖ P ≠ ∅

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ X = ⋃ J
2 1 islp ⊢ J ∈ Top ∧ S ⊆ X → P ∈ limPt ⁡ J ⁡ S ↔ P ∈ cls ⁡ J ⁡ S ∖ P
3 2 3adant3 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ limPt ⁡ J ⁡ S ↔ P ∈ cls ⁡ J ⁡ S ∖ P
4 ssdifss ⊢ S ⊆ X → S ∖ P ⊆ X
5 1 neindisj2 ⊢ J ∈ Top ∧ S ∖ P ⊆ X ∧ P ∈ X → P ∈ cls ⁡ J ⁡ S ∖ P ↔ ∀ n ∈ nei ⁡ J ⁡ P n ∩ S ∖ P ≠ ∅
6 4 5 syl3an2 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ cls ⁡ J ⁡ S ∖ P ↔ ∀ n ∈ nei ⁡ J ⁡ P n ∩ S ∖ P ≠ ∅
7 3 6 bitrd ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ limPt ⁡ J ⁡ S ↔ ∀ n ∈ nei ⁡ J ⁡ P n ∩ S ∖ P ≠ ∅