Metamath Proof Explorer

Theorem flimss2

Description: A limit point of a filter is a limit point of a finer filter. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion flimss2 
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) -> ( J fLim G ) C_ ( J fLim F ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 flimelbas 
 |-  ( x e. ( J fLim G ) -> x e. U. J )
3 2 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> x e. U. J )
4 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> J e. ( TopOn ` X ) )
5 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
6 4 5 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> X = U. J )
7 3 6 eleqtrrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> x e. X )
8 flimneiss 
 |-  ( x e. ( J fLim G ) -> ( ( nei ` J ) ` { x } ) C_ G )
9 8 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> ( ( nei ` J ) ` { x } ) C_ G )
10 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> G C_ F )
11 9 10 sstrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> ( ( nei ` J ) ` { x } ) C_ F )
12 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> F e. ( Fil ` X ) )
13 elflim 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( x e. ( J fLim F ) <-> ( x e. X /\ ( ( nei ` J ) ` { x } ) C_ F ) ) )
14 4 12 13 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> ( x e. ( J fLim F ) <-> ( x e. X /\ ( ( nei ` J ) ` { x } ) C_ F ) ) )
15 7 11 14 mpbir2and 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) /\ x e. ( J fLim G ) ) -> x e. ( J fLim F ) )
16 15 ex 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) -> ( x e. ( J fLim G ) -> x e. ( J fLim F ) ) )
17 16 ssrdv 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) -> ( J fLim G ) C_ ( J fLim F ) )