Metamath Proof Explorer

Theorem flimclsi

Description: The convergent points of a filter are a subset of the closure of any of the filter sets. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion flimclsi 
|- ( S e. F -> ( J fLim F ) C_ ( ( cls ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 flimfil 
 |-  ( x e. ( J fLim F ) -> F e. ( Fil ` U. J ) )
3 2 ad2antlr 
 |-  ( ( ( S e. F /\ x e. ( J fLim F ) ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> F e. ( Fil ` U. J ) )
4 flimnei 
 |-  ( ( x e. ( J fLim F ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> y e. F )
5 4 adantll 
 |-  ( ( ( S e. F /\ x e. ( J fLim F ) ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> y e. F )
6 simpll 
 |-  ( ( ( S e. F /\ x e. ( J fLim F ) ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> S e. F )
7 filinn0 
 |-  ( ( F e. ( Fil ` U. J ) /\ y e. F /\ S e. F ) -> ( y i^i S ) =/= (/) )
8 3 5 6 7 syl3anc 
 |-  ( ( ( S e. F /\ x e. ( J fLim F ) ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> ( y i^i S ) =/= (/) )
9 8 ralrimiva 
 |-  ( ( S e. F /\ x e. ( J fLim F ) ) -> A. y e. ( ( nei ` J ) ` { x } ) ( y i^i S ) =/= (/) )
10 flimtop 
 |-  ( x e. ( J fLim F ) -> J e. Top )
11 10 adantl 
 |-  ( ( S e. F /\ x e. ( J fLim F ) ) -> J e. Top )
12 filelss 
 |-  ( ( F e. ( Fil ` U. J ) /\ S e. F ) -> S C_ U. J )
13 12 ancoms 
 |-  ( ( S e. F /\ F e. ( Fil ` U. J ) ) -> S C_ U. J )
14 2 13 sylan2 
 |-  ( ( S e. F /\ x e. ( J fLim F ) ) -> S C_ U. J )
15 1 flimelbas 
 |-  ( x e. ( J fLim F ) -> x e. U. J )
16 15 adantl 
 |-  ( ( S e. F /\ x e. ( J fLim F ) ) -> x e. U. J )
17 1 neindisj2 
 |-  ( ( J e. Top /\ S C_ U. J /\ x e. U. J ) -> ( x e. ( ( cls ` J ) ` S ) <-> A. y e. ( ( nei ` J ) ` { x } ) ( y i^i S ) =/= (/) ) )
18 11 14 16 17 syl3anc 
 |-  ( ( S e. F /\ x e. ( J fLim F ) ) -> ( x e. ( ( cls ` J ) ` S ) <-> A. y e. ( ( nei ` J ) ` { x } ) ( y i^i S ) =/= (/) ) )
19 9 18 mpbird 
 |-  ( ( S e. F /\ x e. ( J fLim F ) ) -> x e. ( ( cls ` J ) ` S ) )
20 19 ex 
 |-  ( S e. F -> ( x e. ( J fLim F ) -> x e. ( ( cls ` J ) ` S ) ) )
21 20 ssrdv 
 |-  ( S e. F -> ( J fLim F ) C_ ( ( cls ` J ) ` S ) )