Metamath Proof Explorer

Theorem lpval

Description: The set of limit points of a subset of the base set of a topology. Alternate definition of limit point in Munkres p. 97. (Contributed by NM, 10-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis lpfval.1 ⊢ X = ⋃ J
Assertion lpval ⊢ J ∈ Top ∧ S ⊆ X → limPt ⁡ J ⁡ S = x | x ∈ cls ⁡ J ⁡ S ∖ x

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ X = ⋃ J
2 1 lpfval ⊢ J ∈ Top → limPt ⁡ J = y ∈ 𝒫 X ⟼ x | x ∈ cls ⁡ J ⁡ y ∖ x
3 2 fveq1d ⊢ J ∈ Top → limPt ⁡ J ⁡ S = y ∈ 𝒫 X ⟼ x | x ∈ cls ⁡ J ⁡ y ∖ x ⁡ S
4 3 adantr ⊢ J ∈ Top ∧ S ⊆ X → limPt ⁡ J ⁡ S = y ∈ 𝒫 X ⟼ x | x ∈ cls ⁡ J ⁡ y ∖ x ⁡ S
5 eqid ⊢ y ∈ 𝒫 X ⟼ x | x ∈ cls ⁡ J ⁡ y ∖ x = y ∈ 𝒫 X ⟼ x | x ∈ cls ⁡ J ⁡ y ∖ x
6 difeq1 ⊢ y = S → y ∖ x = S ∖ x
7 6 fveq2d ⊢ y = S → cls ⁡ J ⁡ y ∖ x = cls ⁡ J ⁡ S ∖ x
8 7 eleq2d ⊢ y = S → x ∈ cls ⁡ J ⁡ y ∖ x ↔ x ∈ cls ⁡ J ⁡ S ∖ x
9 8 abbidv ⊢ y = S → x | x ∈ cls ⁡ J ⁡ y ∖ x = x | x ∈ cls ⁡ J ⁡ S ∖ x
10 1 topopn ⊢ J ∈ Top → X ∈ J
11 elpw2g ⊢ X ∈ J → S ∈ 𝒫 X ↔ S ⊆ X
12 10 11 syl ⊢ J ∈ Top → S ∈ 𝒫 X ↔ S ⊆ X
13 12 biimpar ⊢ J ∈ Top ∧ S ⊆ X → S ∈ 𝒫 X
14 10 adantr ⊢ J ∈ Top ∧ S ⊆ X → X ∈ J
15 ssdifss ⊢ S ⊆ X → S ∖ x ⊆ X
16 1 clsss3 ⊢ J ∈ Top ∧ S ∖ x ⊆ X → cls ⁡ J ⁡ S ∖ x ⊆ X
17 16 sseld ⊢ J ∈ Top ∧ S ∖ x ⊆ X → x ∈ cls ⁡ J ⁡ S ∖ x → x ∈ X
18 15 17 sylan2 ⊢ J ∈ Top ∧ S ⊆ X → x ∈ cls ⁡ J ⁡ S ∖ x → x ∈ X
19 18 abssdv ⊢ J ∈ Top ∧ S ⊆ X → x | x ∈ cls ⁡ J ⁡ S ∖ x ⊆ X
20 14 19 ssexd ⊢ J ∈ Top ∧ S ⊆ X → x | x ∈ cls ⁡ J ⁡ S ∖ x ∈ V
21 5 9 13 20 fvmptd3 ⊢ J ∈ Top ∧ S ⊆ X → y ∈ 𝒫 X ⟼ x | x ∈ cls ⁡ J ⁡ y ∖ x ⁡ S = x | x ∈ cls ⁡ J ⁡ S ∖ x
22 4 21 eqtrd ⊢ J ∈ Top ∧ S ⊆ X → limPt ⁡ J ⁡ S = x | x ∈ cls ⁡ J ⁡ S ∖ x