Theorem islp2

Description: The predicate " P is a limit point of S " in terms of neighborhoods. Definition of limit point in Munkres p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods. (Contributed by NM, 26-Feb-2007) (Proof shortened by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypothesis	lpfval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	islp2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	⊢ 𝑋 = ∪ 𝐽
2	1	islp	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
3	2	3adant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
4		ssdifss	⊢ ( 𝑆 ⊆ 𝑋 → ( 𝑆 ∖ { 𝑃 } ) ⊆ 𝑋 )
5	1	neindisj2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑃 } ) ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
6	4 5	syl3an2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
7	3 6	bitrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )