Metamath Proof Explorer

Theorem locfincf

Description: A locally finite cover in a coarser topology is locally finite in a finer topology. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis locfincf.1 
|- X = U. J
Assertion locfincf 
|- ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( LocFin ` J ) C_ ( LocFin ` K ) )

Proof

Step Hyp Ref Expression
1 locfincf.1 
 |-  X = U. J
2 topontop 
 |-  ( K e. ( TopOn ` X ) -> K e. Top )
3 2 ad2antrr 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> K e. Top )
4 toponuni 
 |-  ( K e. ( TopOn ` X ) -> X = U. K )
5 4 ad2antrr 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> X = U. K )
6 eqid 
 |-  U. x = U. x
7 1 6 locfinbas 
 |-  ( x e. ( LocFin ` J ) -> X = U. x )
8 7 adantl 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> X = U. x )
9 5 8 eqtr3d 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> U. K = U. x )
10 5 eleq2d 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> ( y e. X <-> y e. U. K ) )
11 1 locfinnei 
 |-  ( ( x e. ( LocFin ` J ) /\ y e. X ) -> E. n e. J ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) )
12 11 ex 
 |-  ( x e. ( LocFin ` J ) -> ( y e. X -> E. n e. J ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) ) )
13 ssrexv 
 |-  ( J C_ K -> ( E. n e. J ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) -> E. n e. K ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) ) )
14 13 adantl 
 |-  ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( E. n e. J ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) -> E. n e. K ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) ) )
15 12 14 sylan9r 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> ( y e. X -> E. n e. K ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) ) )
16 10 15 sylbird 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> ( y e. U. K -> E. n e. K ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) ) )
17 16 ralrimiv 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> A. y e. U. K E. n e. K ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) )
18 eqid 
 |-  U. K = U. K
19 18 6 islocfin 
 |-  ( x e. ( LocFin ` K ) <-> ( K e. Top /\ U. K = U. x /\ A. y e. U. K E. n e. K ( y e. n /\ { s e. x | ( s i^i n ) =/= (/) } e. Fin ) ) )
20 3 9 17 19 syl3anbrc 
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ x e. ( LocFin ` J ) ) -> x e. ( LocFin ` K ) )
21 20 ex 
 |-  ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( x e. ( LocFin ` J ) -> x e. ( LocFin ` K ) ) )
22 21 ssrdv 
 |-  ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( LocFin ` J ) C_ ( LocFin ` K ) )