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

Metamath Proof Explorer

Theorem islpi

Description: A point belonging to a set's closure but not the set itself is a limit point. (Contributed by NM, 8-Nov-2007)

Ref Expression
Hypothesis lpfval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion islpi ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ ¬ 𝑃 ∈ 𝑆 ) ) → 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 clslp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
3 2 eleq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
4 elun ⊢ ( 𝑃 ∈ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( 𝑃 ∈ 𝑆 ∨ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
5 df-or ⊢ ( ( 𝑃 ∈ 𝑆 ∨ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ¬ 𝑃 ∈ 𝑆 → 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
6 4 5 bitri ⊢ ( 𝑃 ∈ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ¬ 𝑃 ∈ 𝑆 → 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
7 3 6 bitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( ¬ 𝑃 ∈ 𝑆 → 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
8 7 biimpd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ( ¬ 𝑃 ∈ 𝑆 → 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
9 8 imp32 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ ¬ 𝑃 ∈ 𝑆 ) ) → 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )