Metamath Proof Explorer

Theorem lpdifsn

Description: P is a limit point of S iff it is a limit point of S \ { P } . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis lpfval.1 ⊢ X = ⋃ J
Assertion lpdifsn ⊢ J ∈ Top ∧ S ⊆ X → P ∈ limPt ⁡ J ⁡ S ↔ P ∈ limPt ⁡ J ⁡ 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 ssdifss ⊢ S ⊆ X → S ∖ P ⊆ X
4 1 islp ⊢ J ∈ Top ∧ S ∖ P ⊆ X → P ∈ limPt ⁡ J ⁡ S ∖ P ↔ P ∈ cls ⁡ J ⁡ S ∖ P ∖ P
5 3 4 sylan2 ⊢ J ∈ Top ∧ S ⊆ X → P ∈ limPt ⁡ J ⁡ S ∖ P ↔ P ∈ cls ⁡ J ⁡ S ∖ P ∖ P
6 difabs ⊢ S ∖ P ∖ P = S ∖ P
7 6 fveq2i ⊢ cls ⁡ J ⁡ S ∖ P ∖ P = cls ⁡ J ⁡ S ∖ P
8 7 eleq2i ⊢ P ∈ cls ⁡ J ⁡ S ∖ P ∖ P ↔ P ∈ cls ⁡ J ⁡ S ∖ P
9 5 8 bitrdi ⊢ J ∈ Top ∧ S ⊆ X → P ∈ limPt ⁡ J ⁡ S ∖ P ↔ P ∈ cls ⁡ J ⁡ S ∖ P
10 2 9 bitr4d ⊢ J ∈ Top ∧ S ⊆ X → P ∈ limPt ⁡ J ⁡ S ↔ P ∈ limPt ⁡ J ⁡ S ∖ P