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