Theorem finptfin

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

	Ref	Expression
Assertion	finptfin	$$⊢A\in \mathrm{Fin}\to A\in \mathrm{PtFin}$$

Proof

Step	Hyp	Ref	Expression
1		rabfi	$$⊢A\in \mathrm{Fin}\to \left\{y\in A|x\in y\right\}\in \mathrm{Fin}$$
2	1	ralrimivw	$$⊢A\in \mathrm{Fin}\to \forall x\in \bigcup A\left\{y\in A|x\in y\right\}\in \mathrm{Fin}$$
3		eqid	$$⊢\bigcup A=\bigcup A$$
4	3	isptfin	$$⊢A\in \mathrm{Fin}\to \left(A\in \mathrm{PtFin}\leftrightarrow \forall x\in \bigcup A\left\{y\in A|x\in y\right\}\in \mathrm{Fin}\right)$$
5	2 4	mpbird	$$⊢A\in \mathrm{Fin}\to A\in \mathrm{PtFin}$$