Theorem isptfin

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

	Ref	Expression
Hypothesis	isptfin.1	|- X = U. A
Assertion	isptfin	|- ( A e. B -> ( A e. PtFin <-> A. x e. X { y e. A | x e. y } e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		isptfin.1	|- X = U. A
2		unieq	|- ( a = A -> U. a = U. A )
3	2 1	eqtr4di	|- ( a = A -> U. a = X )
4		rabeq	|- ( a = A -> { y e. a | x e. y } = { y e. A | x e. y } )
5	4	eleq1d	|- ( a = A -> ( { y e. a | x e. y } e. Fin <-> { y e. A | x e. y } e. Fin ) )
6	3 5	raleqbidv	|- ( a = A -> ( A. x e. U. a { y e. a | x e. y } e. Fin <-> A. x e. X { y e. A | x e. y } e. Fin ) )
7		df-ptfin	|- PtFin = { a | A. x e. U. a { y e. a | x e. y } e. Fin }
8	6 7	elab2g	|- ( A e. B -> ( A e. PtFin <-> A. x e. X { y e. A | x e. y } e. Fin ) )