Metamath Proof Explorer

Theorem islpi

Description: A point belonging to a set's closure but not the set itself is a limit point. (Contributed by NM, 8-Nov-2007)

Ref Expression
Hypothesis lpfval.1 ⊢ X = ⋃ J
Assertion islpi ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S ∧ ¬ P ∈ S → P ∈ limPt ⁡ J ⁡ S

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ X = ⋃ J
2 1 clslp ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ S = S ∪ limPt ⁡ J ⁡ S
3 2 eleq2d ⊢ J ∈ Top ∧ S ⊆ X → P ∈ cls ⁡ J ⁡ S ↔ P ∈ S ∪ limPt ⁡ J ⁡ S
4 elun ⊢ P ∈ S ∪ limPt ⁡ J ⁡ S ↔ P ∈ S ∨ P ∈ limPt ⁡ J ⁡ S
5 df-or ⊢ P ∈ S ∨ P ∈ limPt ⁡ J ⁡ S ↔ ¬ P ∈ S → P ∈ limPt ⁡ J ⁡ S
6 4 5 bitri ⊢ P ∈ S ∪ limPt ⁡ J ⁡ S ↔ ¬ P ∈ S → P ∈ limPt ⁡ J ⁡ S
7 3 6 bitrdi ⊢ J ∈ Top ∧ S ⊆ X → P ∈ cls ⁡ J ⁡ S ↔ ¬ P ∈ S → P ∈ limPt ⁡ J ⁡ S
8 7 biimpd ⊢ J ∈ Top ∧ S ⊆ X → P ∈ cls ⁡ J ⁡ S → ¬ P ∈ S → P ∈ limPt ⁡ J ⁡ S
9 8 imp32 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ cls ⁡ J ⁡ S ∧ ¬ P ∈ S → P ∈ limPt ⁡ J ⁡ S