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 ) )