Metamath Proof Explorer

Theorem clslp

Description: The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

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

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 neindisj ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ )
3 2 expr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
4 3 adantr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ¬ 𝑥 ∈ 𝑆 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
5 difsn ⊢ ( ¬ 𝑥 ∈ 𝑆 → ( 𝑆 ∖ { 𝑥 } ) = 𝑆 )
6 5 ineq2d ⊢ ( ¬ 𝑥 ∈ 𝑆 → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑛 ∩ 𝑆 ) )
7 6 neeq1d ⊢ ( ¬ 𝑥 ∈ 𝑆 → ( ( 𝑛 ∩ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ∅ ↔ ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
8 7 adantl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ¬ 𝑥 ∈ 𝑆 ) → ( ( 𝑛 ∩ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ∅ ↔ ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
9 4 8 sylibrd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ¬ 𝑥 ∈ 𝑆 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ∅ ) )
10 9 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ¬ 𝑥 ∈ 𝑆 → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ∅ ) ) )
11 10 ralrimdv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ¬ 𝑥 ∈ 𝑆 → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ∅ ) )
12 simpll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐽 ∈ Top )
13 simplr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑋 )
14 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
15 14 sselda ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑥 ∈ 𝑋 )
16 1 islp2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ∅ ) )
17 12 13 15 16 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ∅ ) )
18 11 17 sylibrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ¬ 𝑥 ∈ 𝑆 → 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
19 18 orrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∈ 𝑆 ∨ 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
20 elun ⊢ ( 𝑥 ∈ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑆 ∨ 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
21 19 20 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑥 ∈ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
22 21 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑥 ∈ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
23 22 ssrdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
24 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
25 1 lpsscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
26 24 25 unssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
27 23 26 eqssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )