This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem locfinnei

Description: A point covered by a locally finite cover has a neighborhood which intersects only finitely many elements of the cover. (Contributed by Jeff Hankins, 21-Jan-2010)

Ref Expression
Hypothesis locfinnei.1 
|- X = U. J
Assertion locfinnei 
|- ( ( A e. ( LocFin ` J ) /\ P e. X ) -> E. n e. J ( P e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )

Proof

Step Hyp Ref Expression
1 locfinnei.1 
 |-  X = U. J
2 eqid 
 |-  U. A = U. A
3 1 2 islocfin 
 |-  ( A e. ( LocFin ` J ) <-> ( J e. Top /\ X = U. A /\ A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) )
4 3 simp3bi 
 |-  ( A e. ( LocFin ` J ) -> A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
5 eleq1 
 |-  ( x = P -> ( x e. n <-> P e. n ) )
6 5 anbi1d 
 |-  ( x = P -> ( ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) <-> ( P e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) )
7 6 rexbidv 
 |-  ( x = P -> ( E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) <-> E. n e. J ( P e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) )
8 7 rspccva 
 |-  ( ( A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) /\ P e. X ) -> E. n e. J ( P e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
9 4 8 sylan 
 |-  ( ( A e. ( LocFin ` J ) /\ P e. X ) -> E. n e. J ( P e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )