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 JTopOnXFFilXJKKfLimFJfLimF

Proof

Step Hyp Ref Expression
1 eqid K=K
2 1 flimelbas xKfLimFxK
3 2 adantl JTopOnXFFilXJKxKfLimFxK
4 simpl2 JTopOnXFFilXJKxKfLimFFFilX
5 filunibas FFilXF=X
6 4 5 syl JTopOnXFFilXJKxKfLimFF=X
7 1 flimfil xKfLimFFFilK
8 7 adantl JTopOnXFFilXJKxKfLimFFFilK
9 filunibas FFilKF=K
10 8 9 syl JTopOnXFFilXJKxKfLimFF=K
11 6 10 eqtr3d JTopOnXFFilXJKxKfLimFX=K
12 3 11 eleqtrrd JTopOnXFFilXJKxKfLimFxX
13 simpl1 JTopOnXFFilXJKxKfLimFJTopOnX
14 topontop JTopOnXJTop
15 13 14 syl JTopOnXFFilXJKxKfLimFJTop
16 flimtop xKfLimFKTop
17 16 adantl JTopOnXFFilXJKxKfLimFKTop
18 toponuni JTopOnXX=J
19 13 18 syl JTopOnXFFilXJKxKfLimFX=J
20 19 11 eqtr3d JTopOnXFFilXJKxKfLimFJ=K
21 simpl3 JTopOnXFFilXJKxKfLimFJK
22 eqid J=J
23 22 1 topssnei JTopKTopJ=KJKneiJxneiKx
24 15 17 20 21 23 syl31anc JTopOnXFFilXJKxKfLimFneiJxneiKx
25 flimneiss xKfLimFneiKxF
26 25 adantl JTopOnXFFilXJKxKfLimFneiKxF
27 24 26 sstrd JTopOnXFFilXJKxKfLimFneiJxF
28 elflim JTopOnXFFilXxJfLimFxXneiJxF
29 13 4 28 syl2anc JTopOnXFFilXJKxKfLimFxJfLimFxXneiJxF
30 12 27 29 mpbir2and JTopOnXFFilXJKxKfLimFxJfLimF
31 30 ex JTopOnXFFilXJKxKfLimFxJfLimF
32 31 ssrdv JTopOnXFFilXJKKfLimFJfLimF