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 ⊢ 𝑋 = ∪ 𝐽
Assertion lpval ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } )

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 lpfval ⊢ ( 𝐽 ∈ Top → ( limPt ‘ 𝐽 ) = ( 𝑦 ∈ 𝒫 𝑋 ↦ { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) } ) )
3 2 fveq1d ⊢ ( 𝐽 ∈ Top → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑦 ∈ 𝒫 𝑋 ↦ { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) } ) ‘ 𝑆 ) )
4 3 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑦 ∈ 𝒫 𝑋 ↦ { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) } ) ‘ 𝑆 ) )
5 eqid ⊢ ( 𝑦 ∈ 𝒫 𝑋 ↦ { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) } ) = ( 𝑦 ∈ 𝒫 𝑋 ↦ { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) } )
6 difeq1 ⊢ ( 𝑦 = 𝑆 → ( 𝑦 ∖ { 𝑥 } ) = ( 𝑆 ∖ { 𝑥 } ) )
7 6 fveq2d ⊢ ( 𝑦 = 𝑆 → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
8 7 eleq2d ⊢ ( 𝑦 = 𝑆 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
9 8 abbidv ⊢ ( 𝑦 = 𝑆 → { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) } = { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } )
10 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
11 elpw2g ⊢ ( 𝑋 ∈ 𝐽 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
12 10 11 syl ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
13 12 biimpar ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
14 10 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 ∈ 𝐽 )
15 ssdifss ⊢ ( 𝑆 ⊆ 𝑋 → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 )
16 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊆ 𝑋 )
17 16 sseld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) → 𝑥 ∈ 𝑋 ) )
18 15 17 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) → 𝑥 ∈ 𝑋 ) )
19 18 abssdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } ⊆ 𝑋 )
20 14 19 ssexd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } ∈ V )
21 5 9 13 20 fvmptd3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑦 ∈ 𝒫 𝑋 ↦ { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ∖ { 𝑥 } ) ) } ) ‘ 𝑆 ) = { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } )
22 4 21 eqtrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } )