Metamath Proof Explorer

Theorem islp3

Description: The predicate " P is a limit point of S " in terms of open sets. see islp2 , elcls , islp . (Contributed by FL, 31-Jul-2009)

Ref Expression
Hypothesis lpfval.1 ⊢ X = ⋃ J
Assertion islp3 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ limPt ⁡ J ⁡ S ↔ ∀ x ∈ J P ∈ x → x ∩ 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 simp2 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → S ⊆ X
5 4 ssdifssd ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → S ∖ P ⊆ X
6 1 elcls ⊢ J ∈ Top ∧ S ∖ P ⊆ X ∧ P ∈ X → P ∈ cls ⁡ J ⁡ S ∖ P ↔ ∀ x ∈ J P ∈ x → x ∩ S ∖ P ≠ ∅
7 5 6 syld3an2 ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ cls ⁡ J ⁡ S ∖ P ↔ ∀ x ∈ J P ∈ x → x ∩ S ∖ P ≠ ∅
8 3 7 bitrd ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ limPt ⁡ J ⁡ S ↔ ∀ x ∈ J P ∈ x → x ∩ S ∖ P ≠ ∅