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 snnzg 
 |-  ( y e. X -> { y } =/= (/) )
24 21 23 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 ) ) -> { y } =/= (/) )
25 neifil 
 |-  ( ( K e. ( TopOn ` X ) /\ { y } C_ X /\ { y } =/= (/) ) -> ( ( nei ` K ) ` { y } ) e. ( Fil ` X ) )
26 15 22 24 25 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 ) )
27 13 14 26 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 } ) ) )
28 neiflim 
 |-  ( ( K e. ( TopOn ` X ) /\ y e. X ) -> y e. ( K fLim ( ( nei ` K ) ` { y } ) ) )
29 15 21 28 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 } ) ) )
30 27 29 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 } ) ) )
31 flimneiss 
 |-  ( y e. ( J fLim ( ( nei ` K ) ` { y } ) ) -> ( ( nei ` J ) ` { y } ) C_ ( ( nei ` K ) ` { y } ) )
32 30 31 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 } ) )
33 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
34 16 33 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 )
35 opnneip 
 |-  ( ( J e. Top /\ x e. J /\ y e. x ) -> x e. ( ( nei ` J ) ` { y } ) )
36 34 17 20 35 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 } ) )
37 32 36 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 } ) )
38 37 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 } ) )
39 38 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 } ) )
40 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 ) )
41 topontop 
 |-  ( K e. ( TopOn ` X ) -> K e. Top )
42 opnnei 
 |-  ( K e. Top -> ( x e. K <-> A. y e. x x e. ( ( nei ` K ) ` { y } ) ) )
43 40 41 42 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 } ) ) )
44 39 43 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 )
45 44 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 ) )
46 45 ssrdv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) -> J C_ K )
47 10 46 impbida 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) )