Metamath Proof Explorer


Theorem islp3

Description: The predicate " P is a limit point of S " in terms of open sets. see islp2 , elcls , islp . (Contributed by FL, 31-Jul-2009)

Ref Expression
Hypothesis lpfval.1 𝑋 = 𝐽
Assertion islp3 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 𝑋 = 𝐽
2 1 islp ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
3 2 3adant3 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ) )
4 simp2 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋 ) → 𝑆𝑋 )
5 4 ssdifssd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋 ) → ( 𝑆 ∖ { 𝑃 } ) ⊆ 𝑋 )
6 1 elcls ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑃 } ) ⊆ 𝑋𝑃𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ) )
7 5 6 syld3an2 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑃 } ) ) ↔ ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ) )
8 3 7 bitrd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥𝐽 ( 𝑃𝑥 → ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ) )