This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lpdifsn

Description: P is a limit point of S iff it is a limit point of S \ { P } . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis lpfval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion lpdifsn ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 islp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
3 ssdifss ⊢ ( 𝑆 ⊆ 𝑋 → ( 𝑆 ∖ { 𝑃 } ) ⊆ 𝑋 )
4 1 islp ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑃 } ) ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑆 ∖ { 𝑃 } ) ∖ { 𝑃 } ) ) ) )
5 3 4 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑆 ∖ { 𝑃 } ) ∖ { 𝑃 } ) ) ) )
6 difabs ⊢ ( ( 𝑆 ∖ { 𝑃 } ) ∖ { 𝑃 } ) = ( 𝑆 ∖ { 𝑃 } )
7 6 fveq2i ⊢ ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑆 ∖ { 𝑃 } ) ∖ { 𝑃 } ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) )
8 7 eleq2i ⊢ ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑆 ∖ { 𝑃 } ) ∖ { 𝑃 } ) ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) )
9 5 8 bitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
10 2 9 bitr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )