Metamath Proof Explorer

Theorem flimsncls

Description: If A is a limit point of the filter F , then all the points which specialize A (in the specialization preorder) are also limit points. Thus, the set of limit points is a union of closed sets (although this is only nontrivial for non-T1 spaces). (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Assertion flimsncls ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( 𝐽 fLim 𝐹 ) )

Proof

Step Hyp Ref Expression
1 flimtop ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐽 ∈ Top )
2 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
3 2 flimelbas ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐴 ∈ ∪ 𝐽 )
4 3 snssd ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → { 𝐴 } ⊆ ∪ 𝐽 )
5 2 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ { 𝐴 } ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ∪ 𝐽 )
6 1 4 5 syl2anc ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ∪ 𝐽 )
7 6 sselda ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑥 ∈ ∪ 𝐽 )
8 simpll ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) )
9 8 1 syl ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝐽 ∈ Top )
10 simprl ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ∈ 𝐽 )
11 1 adantr ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐽 ∈ Top )
12 4 adantr ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → { 𝐴 } ⊆ ∪ 𝐽 )
13 simpr ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) )
14 11 12 13 3jca ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐽 ∈ Top ∧ { 𝐴 } ⊆ ∪ 𝐽 ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
15 2 clsndisj ⊢ ( ( ( 𝐽 ∈ Top ∧ { 𝐴 } ⊆ ∪ 𝐽 ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → ( 𝑦 ∩ { 𝐴 } ) ≠ ∅ )
16 disjsn ⊢ ( ( 𝑦 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ 𝑦 )
17 16 necon2abii ⊢ ( 𝐴 ∈ 𝑦 ↔ ( 𝑦 ∩ { 𝐴 } ) ≠ ∅ )
18 15 17 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ { 𝐴 } ⊆ ∪ 𝐽 ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝐴 ∈ 𝑦 )
19 14 18 sylan ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝐴 ∈ 𝑦 )
20 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) → 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
21 9 10 19 20 syl3anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
22 flimnei ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑦 ∈ 𝐹 )
23 8 21 22 syl2anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ∈ 𝐹 )
24 23 expr ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) )
25 24 ralrimiva ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) )
26 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
27 11 26 sylib ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
28 2 flimfil ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
29 28 adantr ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
30 flimopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
31 27 29 30 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
32 7 25 31 mpbir2and ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )
33 32 ex ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) )
34 33 ssrdv ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( 𝐽 fLim 𝐹 ) )