Metamath Proof Explorer

Theorem lfinpfin

Description: A locally finite cover is point-finite. (Contributed by Jeff Hankins, 21-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion lfinpfin 
|- ( A e. ( LocFin ` J ) -> A e. PtFin )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 eqid 
 |-  U. A = U. A
3 1 2 locfinbas 
 |-  ( A e. ( LocFin ` J ) -> U. J = U. A )
4 3 eleq2d 
 |-  ( A e. ( LocFin ` J ) -> ( x e. U. J <-> x e. U. A ) )
5 4 biimpar 
 |-  ( ( A e. ( LocFin ` J ) /\ x e. U. A ) -> x e. U. J )
6 1 locfinnei 
 |-  ( ( A e. ( LocFin ` J ) /\ x e. U. J ) -> E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
7 5 6 syldan 
 |-  ( ( A e. ( LocFin ` J ) /\ x e. U. A ) -> E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
8 inelcm 
 |-  ( ( x e. s /\ x e. n ) -> ( s i^i n ) =/= (/) )
9 8 expcom 
 |-  ( x e. n -> ( x e. s -> ( s i^i n ) =/= (/) ) )
10 9 ad2antlr 
 |-  ( ( ( ( A e. ( LocFin ` J ) /\ x e. U. A ) /\ x e. n ) /\ s e. A ) -> ( x e. s -> ( s i^i n ) =/= (/) ) )
11 10 ss2rabdv 
 |-  ( ( ( A e. ( LocFin ` J ) /\ x e. U. A ) /\ x e. n ) -> { s e. A | x e. s } C_ { s e. A | ( s i^i n ) =/= (/) } )
12 ssfi 
 |-  ( ( { s e. A | ( s i^i n ) =/= (/) } e. Fin /\ { s e. A | x e. s } C_ { s e. A | ( s i^i n ) =/= (/) } ) -> { s e. A | x e. s } e. Fin )
13 12 expcom 
 |-  ( { s e. A | x e. s } C_ { s e. A | ( s i^i n ) =/= (/) } -> ( { s e. A | ( s i^i n ) =/= (/) } e. Fin -> { s e. A | x e. s } e. Fin ) )
14 11 13 syl 
 |-  ( ( ( A e. ( LocFin ` J ) /\ x e. U. A ) /\ x e. n ) -> ( { s e. A | ( s i^i n ) =/= (/) } e. Fin -> { s e. A | x e. s } e. Fin ) )
15 14 expimpd 
 |-  ( ( A e. ( LocFin ` J ) /\ x e. U. A ) -> ( ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) -> { s e. A | x e. s } e. Fin ) )
16 15 rexlimdvw 
 |-  ( ( A e. ( LocFin ` J ) /\ x e. U. A ) -> ( E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) -> { s e. A | x e. s } e. Fin ) )
17 7 16 mpd 
 |-  ( ( A e. ( LocFin ` J ) /\ x e. U. A ) -> { s e. A | x e. s } e. Fin )
18 17 ralrimiva 
 |-  ( A e. ( LocFin ` J ) -> A. x e. U. A { s e. A | x e. s } e. Fin )
19 2 isptfin 
 |-  ( A e. ( LocFin ` J ) -> ( A e. PtFin <-> A. x e. U. A { s e. A | x e. s } e. Fin ) )
20 18 19 mpbird 
 |-  ( A e. ( LocFin ` J ) -> A e. PtFin )