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=\bigcup A$$
Assertion	ptfinfin	$$⊢\left(A\in \mathrm{PtFin}\wedge P\in X\right)\to \left\{x\in A|P\in x\right\}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		ptfinfin.1	$$⊢X=\bigcup A$$
2	1	isptfin	$$⊢A\in \mathrm{PtFin}\to \left(A\in \mathrm{PtFin}\leftrightarrow \forall p\in X\left\{x\in A|p\in x\right\}\in \mathrm{Fin}\right)$$
3	2	ibi	$$⊢A\in \mathrm{PtFin}\to \forall p\in X\left\{x\in A|p\in x\right\}\in \mathrm{Fin}$$
4		eleq1	$$⊢p=P\to \left(p\in x\leftrightarrow P\in x\right)$$
5	4	rabbidv	$$⊢p=P\to \left\{x\in A|p\in x\right\}=\left\{x\in A|P\in x\right\}$$
6	5	eleq1d	$$⊢p=P\to \left(\left\{x\in A|p\in x\right\}\in \mathrm{Fin}\leftrightarrow \left\{x\in A|P\in x\right\}\in \mathrm{Fin}\right)$$
7	6	rspccv	$$⊢\forall p\in X\left\{x\in A|p\in x\right\}\in \mathrm{Fin}\to \left(P\in X\to \left\{x\in A|P\in x\right\}\in \mathrm{Fin}\right)$$
8	3 7	syl	$$⊢A\in \mathrm{PtFin}\to \left(P\in X\to \left\{x\in A|P\in x\right\}\in \mathrm{Fin}\right)$$
9	8	imp	$$⊢\left(A\in \mathrm{PtFin}\wedge P\in X\right)\to \left\{x\in A|P\in x\right\}\in \mathrm{Fin}$$