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 ) ) )