Metamath Proof Explorer


Theorem flimcf

Description: Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion flimcf JTopOnXKTopOnXJKfFilXKfLimfJfLimf

Proof

Step Hyp Ref Expression
1 simplll JTopOnXKTopOnXJKfFilXxKfLimfJTopOnX
2 simprl JTopOnXKTopOnXJKfFilXxKfLimffFilX
3 simplr JTopOnXKTopOnXJKfFilXxKfLimfJK
4 flimss1 JTopOnXfFilXJKKfLimfJfLimf
5 1 2 3 4 syl3anc JTopOnXKTopOnXJKfFilXxKfLimfKfLimfJfLimf
6 simprr JTopOnXKTopOnXJKfFilXxKfLimfxKfLimf
7 5 6 sseldd JTopOnXKTopOnXJKfFilXxKfLimfxJfLimf
8 7 expr JTopOnXKTopOnXJKfFilXxKfLimfxJfLimf
9 8 ssrdv JTopOnXKTopOnXJKfFilXKfLimfJfLimf
10 9 ralrimiva JTopOnXKTopOnXJKfFilXKfLimfJfLimf
11 oveq2 f=neiKyKfLimf=KfLimneiKy
12 oveq2 f=neiKyJfLimf=JfLimneiKy
13 11 12 sseq12d f=neiKyKfLimfJfLimfKfLimneiKyJfLimneiKy
14 simplr JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxfFilXKfLimfJfLimf
15 simpllr JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxKTopOnX
16 simplll JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxJTopOnX
17 simprl JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxxJ
18 toponss JTopOnXxJxX
19 16 17 18 syl2anc JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxxX
20 simprr JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxyx
21 19 20 sseldd JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxyX
22 21 snssd JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxyX
23 20 snn0d JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxy
24 neifil KTopOnXyXyneiKyFilX
25 15 22 23 24 syl3anc JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxneiKyFilX
26 13 14 25 rspcdva JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxKfLimneiKyJfLimneiKy
27 neiflim KTopOnXyXyKfLimneiKy
28 15 21 27 syl2anc JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxyKfLimneiKy
29 26 28 sseldd JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxyJfLimneiKy
30 flimneiss yJfLimneiKyneiJyneiKy
31 29 30 syl JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxneiJyneiKy
32 topontop JTopOnXJTop
33 16 32 syl JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxJTop
34 opnneip JTopxJyxxneiJy
35 33 17 20 34 syl3anc JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxxneiJy
36 31 35 sseldd JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxxneiKy
37 36 anassrs JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxxneiKy
38 37 ralrimiva JTopOnXKTopOnXfFilXKfLimfJfLimfxJyxxneiKy
39 simpllr JTopOnXKTopOnXfFilXKfLimfJfLimfxJKTopOnX
40 topontop KTopOnXKTop
41 opnnei KTopxKyxxneiKy
42 39 40 41 3syl JTopOnXKTopOnXfFilXKfLimfJfLimfxJxKyxxneiKy
43 38 42 mpbird JTopOnXKTopOnXfFilXKfLimfJfLimfxJxK
44 43 ex JTopOnXKTopOnXfFilXKfLimfJfLimfxJxK
45 44 ssrdv JTopOnXKTopOnXfFilXKfLimfJfLimfJK
46 10 45 impbida JTopOnXKTopOnXJKfFilXKfLimfJfLimf