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