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
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) )

Proof

Step Hyp Ref Expression
1 simplll
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> J e. ( TopOn ` X ) )
2 simprl
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> f e. ( Fil ` X ) )
3 simplr
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> J C_ K )
4 flimss1
 |-  ( ( J e. ( TopOn ` X ) /\ f e. ( Fil ` X ) /\ J C_ K ) -> ( K fLim f ) C_ ( J fLim f ) )
5 1 2 3 4 syl3anc
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> ( K fLim f ) C_ ( J fLim f ) )
6 simprr
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> x e. ( K fLim f ) )
7 5 6 sseldd
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> x e. ( J fLim f ) )
8 7 expr
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ f e. ( Fil ` X ) ) -> ( x e. ( K fLim f ) -> x e. ( J fLim f ) ) )
9 8 ssrdv
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ f e. ( Fil ` X ) ) -> ( K fLim f ) C_ ( J fLim f ) )
10 9 ralrimiva
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) -> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) )
11 oveq2
 |-  ( f = ( ( nei ` K ) ` { y } ) -> ( K fLim f ) = ( K fLim ( ( nei ` K ) ` { y } ) ) )
12 oveq2
 |-  ( f = ( ( nei ` K ) ` { y } ) -> ( J fLim f ) = ( J fLim ( ( nei ` K ) ` { y } ) ) )
13 11 12 sseq12d
 |-  ( f = ( ( nei ` K ) ` { y } ) -> ( ( K fLim f ) C_ ( J fLim f ) <-> ( K fLim ( ( nei ` K ) ` { y } ) ) C_ ( J fLim ( ( nei ` K ) ` { y } ) ) ) )
14 simplr
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) )
15 simpllr
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> K e. ( TopOn ` X ) )
16 simplll
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> J e. ( TopOn ` X ) )
17 simprl
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> x e. J )
18 toponss
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
19 16 17 18 syl2anc
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> x C_ X )
20 simprr
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> y e. x )
21 19 20 sseldd
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> y e. X )
22 21 snssd
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> { y } C_ X )
23 20 snn0d
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> { y } =/= (/) )
24 neifil
 |-  ( ( K e. ( TopOn ` X ) /\ { y } C_ X /\ { y } =/= (/) ) -> ( ( nei ` K ) ` { y } ) e. ( Fil ` X ) )
25 15 22 23 24 syl3anc
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> ( ( nei ` K ) ` { y } ) e. ( Fil ` X ) )
26 13 14 25 rspcdva
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> ( K fLim ( ( nei ` K ) ` { y } ) ) C_ ( J fLim ( ( nei ` K ) ` { y } ) ) )
27 neiflim
 |-  ( ( K e. ( TopOn ` X ) /\ y e. X ) -> y e. ( K fLim ( ( nei ` K ) ` { y } ) ) )
28 15 21 27 syl2anc
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> y e. ( K fLim ( ( nei ` K ) ` { y } ) ) )
29 26 28 sseldd
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> y e. ( J fLim ( ( nei ` K ) ` { y } ) ) )
30 flimneiss
 |-  ( y e. ( J fLim ( ( nei ` K ) ` { y } ) ) -> ( ( nei ` J ) ` { y } ) C_ ( ( nei ` K ) ` { y } ) )
31 29 30 syl
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> ( ( nei ` J ) ` { y } ) C_ ( ( nei ` K ) ` { y } ) )
32 topontop
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
33 16 32 syl
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> J e. Top )
34 opnneip
 |-  ( ( J e. Top /\ x e. J /\ y e. x ) -> x e. ( ( nei ` J ) ` { y } ) )
35 33 17 20 34 syl3anc
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> x e. ( ( nei ` J ) ` { y } ) )
36 31 35 sseldd
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> x e. ( ( nei ` K ) ` { y } ) )
37 36 anassrs
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) /\ y e. x ) -> x e. ( ( nei ` K ) ` { y } ) )
38 37 ralrimiva
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) -> A. y e. x x e. ( ( nei ` K ) ` { y } ) )
39 simpllr
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) -> K e. ( TopOn ` X ) )
40 topontop
 |-  ( K e. ( TopOn ` X ) -> K e. Top )
41 opnnei
 |-  ( K e. Top -> ( x e. K <-> A. y e. x x e. ( ( nei ` K ) ` { y } ) ) )
42 39 40 41 3syl
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) -> ( x e. K <-> A. y e. x x e. ( ( nei ` K ) ` { y } ) ) )
43 38 42 mpbird
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) -> x e. K )
44 43 ex
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) -> ( x e. J -> x e. K ) )
45 44 ssrdv
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) -> J C_ K )
46 10 45 impbida
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) )