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

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

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 lpval ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } )
3 2 eleq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } ) )
4 id ⊢ ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) )
5 id ⊢ ( 𝑥 = 𝑃 → 𝑥 = 𝑃 )
6 sneq ⊢ ( 𝑥 = 𝑃 → { 𝑥 } = { 𝑃 } )
7 6 difeq2d ⊢ ( 𝑥 = 𝑃 → ( 𝑆 ∖ { 𝑥 } ) = ( 𝑆 ∖ { 𝑃 } ) )
8 7 fveq2d ⊢ ( 𝑥 = 𝑃 → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) )
9 5 8 eleq12d ⊢ ( 𝑥 = 𝑃 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
10 4 9 elab3 ⊢ ( 𝑃 ∈ { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) )
11 3 10 bitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )