Theorem ptfinfin

Description: A point covered by a point-finite cover is only covered by finitely many elements. (Contributed by Jeff Hankins, 21-Jan-2010)

	Ref	Expression
Hypothesis	ptfinfin.1	|- X = U. A
Assertion	ptfinfin	|- ( ( A e. PtFin /\ P e. X ) -> { x e. A | P e. x } e. Fin )

Proof

Step	Hyp	Ref	Expression
1		ptfinfin.1	|- X = U. A
2	1	isptfin	|- ( A e. PtFin -> ( A e. PtFin <-> A. p e. X { x e. A | p e. x } e. Fin ) )
3	2	ibi	|- ( A e. PtFin -> A. p e. X { x e. A | p e. x } e. Fin )
4		eleq1	|- ( p = P -> ( p e. x <-> P e. x ) )
5	4	rabbidv	|- ( p = P -> { x e. A | p e. x } = { x e. A | P e. x } )
6	5	eleq1d	|- ( p = P -> ( { x e. A | p e. x } e. Fin <-> { x e. A | P e. x } e. Fin ) )
7	6	rspccv	|- ( A. p e. X { x e. A | p e. x } e. Fin -> ( P e. X -> { x e. A | P e. x } e. Fin ) )
8	3 7	syl	|- ( A e. PtFin -> ( P e. X -> { x e. A | P e. x } e. Fin ) )
9	8	imp	|- ( ( A e. PtFin /\ P e. X ) -> { x e. A | P e. x } e. Fin )