Metamath Proof Explorer

Theorem flimss1

Description: A limit point of a filter is a limit point in a coarser topology. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. K = U. K
2 1 flimelbas 
 |-  ( x e. ( K fLim F ) -> x e. U. K )
3 2 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> x e. U. K )
4 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> F e. ( Fil ` X ) )
5 filunibas 
 |-  ( F e. ( Fil ` X ) -> U. F = X )
6 4 5 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> U. F = X )
7 1 flimfil 
 |-  ( x e. ( K fLim F ) -> F e. ( Fil ` U. K ) )
8 7 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> F e. ( Fil ` U. K ) )
9 filunibas 
 |-  ( F e. ( Fil ` U. K ) -> U. F = U. K )
10 8 9 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> U. F = U. K )
11 6 10 eqtr3d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> X = U. K )
12 3 11 eleqtrrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> x e. X )
13 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> J e. ( TopOn ` X ) )
14 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
15 13 14 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> J e. Top )
16 flimtop 
 |-  ( x e. ( K fLim F ) -> K e. Top )
17 16 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> K e. Top )
18 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
19 13 18 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> X = U. J )
20 19 11 eqtr3d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> U. J = U. K )
21 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> J C_ K )
22 eqid 
 |-  U. J = U. J
23 22 1 topssnei 
 |-  ( ( ( J e. Top /\ K e. Top /\ U. J = U. K ) /\ J C_ K ) -> ( ( nei ` J ) ` { x } ) C_ ( ( nei ` K ) ` { x } ) )
24 15 17 20 21 23 syl31anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> ( ( nei ` J ) ` { x } ) C_ ( ( nei ` K ) ` { x } ) )
25 flimneiss 
 |-  ( x e. ( K fLim F ) -> ( ( nei ` K ) ` { x } ) C_ F )
26 25 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> ( ( nei ` K ) ` { x } ) C_ F )
27 24 26 sstrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> ( ( nei ` J ) ` { x } ) C_ F )
28 elflim 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( x e. ( J fLim F ) <-> ( x e. X /\ ( ( nei ` J ) ` { x } ) C_ F ) ) )
29 13 4 28 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> ( x e. ( J fLim F ) <-> ( x e. X /\ ( ( nei ` J ) ` { x } ) C_ F ) ) )
30 12 27 29 mpbir2and 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fLim F ) ) -> x e. ( J fLim F ) )
31 30 ex 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) -> ( x e. ( K fLim F ) -> x e. ( J fLim F ) ) )
32 31 ssrdv 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) -> ( K fLim F ) C_ ( J fLim F ) )