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 
|- ( A e. ( J fLim F ) -> ( ( cls ` J ) ` { A } ) C_ ( J fLim F ) )

Proof

Step Hyp Ref Expression
1 flimtop 
 |-  ( A e. ( J fLim F ) -> J e. Top )
2 eqid 
 |-  U. J = U. J
3 2 flimelbas 
 |-  ( A e. ( J fLim F ) -> A e. U. J )
4 3 snssd 
 |-  ( A e. ( J fLim F ) -> { A } C_ U. J )
5 2 clsss3 
 |-  ( ( J e. Top /\ { A } C_ U. J ) -> ( ( cls ` J ) ` { A } ) C_ U. J )
6 1 4 5 syl2anc 
 |-  ( A e. ( J fLim F ) -> ( ( cls ` J ) ` { A } ) C_ U. J )
7 6 sselda 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> x e. U. J )
8 simpll 
 |-  ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> A e. ( J fLim F ) )
9 8 1 syl 
 |-  ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> J e. Top )
10 simprl 
 |-  ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> y e. J )
11 1 adantr 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> J e. Top )
12 4 adantr 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> { A } C_ U. J )
13 simpr 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> x e. ( ( cls ` J ) ` { A } ) )
14 11 12 13 3jca 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> ( J e. Top /\ { A } C_ U. J /\ x e. ( ( cls ` J ) ` { A } ) ) )
15 2 clsndisj 
 |-  ( ( ( J e. Top /\ { A } C_ U. J /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> ( y i^i { A } ) =/= (/) )
16 disjsn 
 |-  ( ( y i^i { A } ) = (/) <-> -. A e. y )
17 16 necon2abii 
 |-  ( A e. y <-> ( y i^i { A } ) =/= (/) )
18 15 17 sylibr 
 |-  ( ( ( J e. Top /\ { A } C_ U. J /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> A e. y )
19 14 18 sylan 
 |-  ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> A e. y )
20 opnneip 
 |-  ( ( J e. Top /\ y e. J /\ A e. y ) -> y e. ( ( nei ` J ) ` { A } ) )
21 9 10 19 20 syl3anc 
 |-  ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> y e. ( ( nei ` J ) ` { A } ) )
22 flimnei 
 |-  ( ( A e. ( J fLim F ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> y e. F )
23 8 21 22 syl2anc 
 |-  ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> y e. F )
24 23 expr 
 |-  ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ y e. J ) -> ( x e. y -> y e. F ) )
25 24 ralrimiva 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> A. y e. J ( x e. y -> y e. F ) )
26 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
27 11 26 sylib 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> J e. ( TopOn ` U. J ) )
28 2 flimfil 
 |-  ( A e. ( J fLim F ) -> F e. ( Fil ` U. J ) )
29 28 adantr 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> F e. ( Fil ` U. J ) )
30 flimopn 
 |-  ( ( J e. ( TopOn ` U. J ) /\ F e. ( Fil ` U. J ) ) -> ( x e. ( J fLim F ) <-> ( x e. U. J /\ A. y e. J ( x e. y -> y e. F ) ) ) )
31 27 29 30 syl2anc 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> ( x e. ( J fLim F ) <-> ( x e. U. J /\ A. y e. J ( x e. y -> y e. F ) ) ) )
32 7 25 31 mpbir2and 
 |-  ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> x e. ( J fLim F ) )
33 32 ex 
 |-  ( A e. ( J fLim F ) -> ( x e. ( ( cls ` J ) ` { A } ) -> x e. ( J fLim F ) ) )
34 33 ssrdv 
 |-  ( A e. ( J fLim F ) -> ( ( cls ` J ) ` { A } ) C_ ( J fLim F ) )