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