Theorem finptfin

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

	Ref	Expression
Assertion	finptfin	|- ( A e. Fin -> A e. PtFin )

Proof

Step	Hyp	Ref	Expression
1		rabfi	|- ( A e. Fin -> { y e. A | x e. y } e. Fin )
2	1	ralrimivw	|- ( A e. Fin -> A. x e. U. A { y e. A | x e. y } e. Fin )
3		eqid	|- U. A = U. A
4	3	isptfin	|- ( A e. Fin -> ( A e. PtFin <-> A. x e. U. A { y e. A | x e. y } e. Fin ) )
5	2 4	mpbird	|- ( A e. Fin -> A e. PtFin )