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 ‘ 𝐽 ) ‘ 𝑆 ) )