Metamath Proof Explorer

Theorem islp

Description: The predicate "the class P is a limit point of S ". (Contributed by NM, 10-Feb-2007)

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

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ X = ⋃ J
2 1 lpval ⊢ J ∈ Top ∧ S ⊆ X → limPt ⁡ J ⁡ S = x | x ∈ cls ⁡ J ⁡ S ∖ x
3 2 eleq2d ⊢ J ∈ Top ∧ S ⊆ X → P ∈ limPt ⁡ J ⁡ S ↔ P ∈ x | x ∈ cls ⁡ J ⁡ S ∖ x
4 id ⊢ P ∈ cls ⁡ J ⁡ S ∖ P → P ∈ cls ⁡ J ⁡ S ∖ P
5 id ⊢ x = P → x = P
6 sneq ⊢ x = P → x = P
7 6 difeq2d ⊢ x = P → S ∖ x = S ∖ P
8 7 fveq2d ⊢ x = P → cls ⁡ J ⁡ S ∖ x = cls ⁡ J ⁡ S ∖ P
9 5 8 eleq12d ⊢ x = P → x ∈ cls ⁡ J ⁡ S ∖ x ↔ P ∈ cls ⁡ J ⁡ S ∖ P
10 4 9 elab3 ⊢ P ∈ x | x ∈ cls ⁡ J ⁡ S ∖ x ↔ P ∈ cls ⁡ J ⁡ S ∖ P
11 3 10 bitrdi ⊢ J ∈ Top ∧ S ⊆ X → P ∈ limPt ⁡ J ⁡ S ↔ P ∈ cls ⁡ J ⁡ S ∖ P